[Agda] Re: Syntax for anonymous functions

[Jean-Philippe Bernardy]

On Thu, May 26, 2011 at 11:02 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:

> My gut feeling is that syntax is getting a bit to diverse now.  If we embrace the |->, we should drop
> the \lambda (that would make a function syntax similar to scala).

Yes!

>  function
>     {A = Int}  (c x)         y -> ...
>     {A = Bool} (d x (a , b)) y -> ...

I like the "function" thing too; but please use the "=" sign there.
This means more consistency (and "manual lambda lifting" easier).

Cheers,
JP.