[Agda] Absurd lambdas

[Ulf Norell]

On Tue, Oct 28, 2008 at 3:44 PM, Noam Zeilberger
<noam+agda at cs.cmu.edu<noam%2Bagda at cs.cmu.edu>
> wrote:

> 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


Yes, there is something to that. I'll have a think about it.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20081028/32205a73/attachment.html