Re: [Agda] : vs. ∶
Darryl
psygnisfive at yahoo.com
Fri Nov 30 00:07:47 CET 2012
Why not use `as` instead of `\:`? After all, the use of `\:` is to state the type of an ambiguous term when using it, so what `\x -> x \: A -> A` means is that we're using `\x -> x` AS a function of type `A -> A`. So you could just write `\x -> x as A -> A`. This is
- darryl
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121129/aa41f54b/attachment.html
More information about the Agda
mailing list