Re: [Agda] : vs. ∶

Darryl psygnisfive at
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...

More information about the Agda mailing list