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

Darin Morrison darinmorrison at gmail.com
Sat May 7 05:08:13 CEST 2011


On 7 May 2011, at 02:54, Fredrik Nordvall Forsberg wrote:

>> Is the grammar ambiguous? I don't think we should let our tools dictate
>> the design of the language.
> 
> No, I've finally convinced our tools that it is not. Thus the syntax is now
> 
>   and = \ ( true x -> x ; false _ -> false )
> 
> which I, from the response on the mailing list, judge to be the right syntax
> when it comes to '->' vs. '='. What about the rest of the syntax? At AIM
> XIII, we were originally aiming for 
> 
>   and = \ { true x -> x ; false _ -> false }

The second one is the version I prefer since it matches the style used for records whereas the other version would look strange when split across multiple lines.

- Darin



More information about the Agda mailing list