[Agda] Re: Forall and product

[Andrea Vezzosi]

By the way, "forall x -> B x" is simply syntactic sugar for "(x : _)
-> B x", where the "_" tells Agda to (try to) infer what should go
there, which is the type of "x".


Cheers,
Andrea

On Tue, Feb 17, 2015 at 10:57 AM, N. Raghavendra <raghu at hri.res.in> wrote:
> 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/
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda