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

[Anthony de Almeida Lopes]

For the record, I am with Andreas on this...

2011/5/5 Dan Licata <drl at cs.cmu.edu>:
> 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.
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>