[Agda] nameless pattern-matching functions

[Nils Anders Danielsson]

On Thu, Mar 6, 2008 at 12:49 PM, Noam Zeilberger <noam+agda at cs.cmu.edu> wrote:

> I often run into situations where I would like to create a nameless
> function using pattern-matching, but am forced to give it a name.

I agree that this is sometimes annoying; pattern-matching definitions
are not really first-class.

>  Would it be tricky to extend Agda to allow pattern-matching in
>  nameless functions?

In the simply typed case I don't think it would be very hard (you may
have to give a type signature for the domain of the function).
However, in the dependently typed case matching on an expression can
lead to variables in an outer scope becoming instantiated. You may
have noticed this when using "with", for instance. One could invent
some syntax which takes this into account, I suppose, but I fear it
would be rather heavyweight.

-- 
/NAD