[Agda] Absurd lambdas

[Ulf Norell]

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

The usual lambda sugar applies, with the restriction that the absurd pattern
must be the last argument:

  \x y ()    -- OK
  \x () y    -- Not OK (but \x () will do)

Here's a simple motivating example:

¬_ : Set -> Set
¬ A = A -> False

compare : (x y : Bool) -> (x == y) ∨ ¬ (x == y)
compare true  true  = inl refl
compare true  false = inr \()    -- \() : true == false -> False
compare false true  = inr \()    -- \() : false == true -> False
compare false false = inl refl

Internally, the type checker replaces the absurd lambda by a call to the
function you would otherwise define by hand.

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