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

[Nils Anders Danielsson]

On 2011-05-07 06:31, wren ng thornton wrote:
> I'm sure it's old history, but what reasons are there for avoiding the
> use of a period for these kind of binders (as is done in mathematical
> notation)?

Agda does it for consistency with Haskell. As far as I know it would be
unproblematic to support the notation

   λ x y z . e

in Agda (with whitespace around the dot). However, I don't think I've
ever seen dots used for definitions by pattern matching, whereas the TRS
literature often uses arrows.

-- 
/NAD