[Agda] Re: Forall and product

[N. Raghavendra]

At 2015-02-16T13:41:11-06:00, Chris Jenkins wrote:

> So Agda sees the f and it's implicit arguments (in your example,
> hidden) {x} {y}, produces the C (x , y) (underscores in your example
> because they were inferred), then thinks you meant to apply this
> result to x and y. Of course, C (x , y) isn't a function type! So
> Agda complains.

Hi Chris,

Thanks very much for the detailed explanation.  So the implicit
arguments put an element of type C(x,y) where a function was expected.
Also, I learnt from your explanation that forall can have explicit
arguments as in \forall x ...; I'd thought wrongly that forall takes
only implicit arguments as in \forall {x}.

Cheers,
Raghu.

-- 
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/