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