[Agda] Handling the Impossible

[Ulf Norell]

On Fri, May 9, 2008 at 4:46 PM, Samuel Bronson <naesten at gmail.com> wrote:

> How do you prove that a type is uninhabited? For example, Fin 0...


There is a special absurd pattern that can be used to match empty types: ()

magic : {A : Set} -> Fin 0 -> A
magic ()

When you match with an absurd pattern you don't have to give a right hand
side.

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