[Agda] Re: Forall and product
N. Raghavendra
raghu at hri.res.in
Tue Feb 17 11:38:52 CET 2015
At 2015-02-17T11:03:12+01:00, Andrea Vezzosi wrote:
> By the way, "forall x -> B x" is simply syntactic sugar for "(x : _)
> -> B x"
I guess I should get used to the fact that it's only syntactic sugar.
Whenever I see "forall x -> B x" I keep thinking "\prod_x B(x)". But I
think of "(x : _) -> B x" also as "\prod_x B(x)", so I guess it's ok.
Cheers,
Raghu.
--
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/
More information about the Agda
mailing list