[Agda] Absurd lambdas

[Noam Zeilberger]

On Tue, Oct 28, 2008 at 01:48:10PM +0100, Ulf Norell wrote:
> Previously, to discharge an element of an empty type you would have to
> define a function which pattern matched on the element using an absurd
> pattern. This can get tedious so now there's a short-hand:
> 
> If A is an empty (constructorless) type then
> 
>  \ () : (x : A) -> B
>  \ {} : {x : A} -> B

Sounds good, but I would say this is a special case of what you want
in general, which is anonymous functions defined by pattern-matching.
See the old thread http://osdir.com/ml/lang.agda/2008-03/msg00007.html

Noam