Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]
wren ng thornton
wren at freegeek.org
Mon May 9 22:06:07 CEST 2011
On 5/9/11 10:28 AM, Andreas Abel wrote:
> Concering juxtaposition-as-application, I must say that I am not really
> fond of the (x y : Nat) -> ... syntax, because that looks like an
> application (x y) in my cerebral pattern matcher.
Indeed. I have to continually rewire my cerebral pattern matcher to
accept that syntax.
> Yet we have it, and so
> we should also have
>
> \ x y -> ...
>
> And Haskell also has it. And the MLs.
This seems most sensible. Requiring parentheses for application in
patterns is just fine by me.
--
Live well,
~wren
More information about the Agda
mailing list