Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]

[Nils Anders Danielsson]

On 2011-05-05 11:32, Andreas Abel wrote:
> One option was not discussed that I want to bring forward:  Introduce a
> new layout keyword.  One possibility would be "function".  That would
> look like
>
>     and = function
>             true  x ->  x
>             false _ ->  false
>
> Without layout:
>
>     and = function { true x ->  x; false _ ->  false }

This is an interesting suggestion.

> Unfortunately, Agda has no means of doing "without layout" (, yet ?!).

I think Agda used to support {;}, but for some reason Ulf removed this
support.

In general I think we should strive for consistency. Karim et alii's
proposal doesn't quite match other parts of the language.

-- 
/NAD