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

[Dan Licata]

In SML, 'fun' declarations are written using 
'fun f p = e | f p2 => e2 | ...' but 'case'
expressions are written using 'case x of p => e | ...'.  
This is often annoyng when you want to refactor one into the other, or
vice versa, because you need to edit all of the separators.  

It would be nice to avoid this problem in Agda, though I don't have any
particular suggestions for the syntax.

-Dan

On May05, Andreas Abel wrote:
> On 05.05.11 3:38 PM, Stefan Monnier wrote:
> >>Can you please remind me why the "->" does not work instead of "=".
> >
> >"->" is consistent with the current \lambda, but "=" is consistent with
> >the top-level definitions.  Your "merge record and function" drift seems
> >to be arguing for the use of "=" rather than "->" since it makes it
> >closer to top-level definitions.
> 
> Well, I have been brought up with using "=" for equations ;-), so I think
> 
>   f x zero = bla
> 
> is fine for top-level definition, since the lhs actually reduces to the 
> rhs (if we are lucky...) and they are treated equal by the type checker.
> 
> But
> 
>   \ x zero = bla ...
> 
> does not look so intuitive.  We are speaking of a function that maps 
> (x,zero) to bla (modulo currying), so I find
> 
>   \ x zero -> bla ...
> 
> better.
>