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

[Nils Anders Danielsson]

On 2011-05-07 03:54, Fredrik Nordvall Forsberg wrote:
> However, I can imagine that this would be hard to achieve the way we currently
> do things -- how does the parser know if "\ true ->  0" should be parsed as a
> traditional lambda with a variable named "true" (as current Agda does) or as
> an incomplete pattern matching lambda (as it then probably should, to be
> consistent with "f : Bool ->  Nat ; f true = 0")?

Lambda-bound variables should not be allowed to shadow constructors:

   http://code.google.com/p/agda/issues/detail?id=297

-- 
/NAD