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