[Agda] Handling the Impossible

[Lennart Augustsson]

Why is there a special pattern?  Wouldn't _ or a variable work?

  -- Lennart

On Fri, May 9, 2008 at 3:48 PM, Ulf Norell <ulfn at cs.chalmers.se> wrote:

>
>
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080509/eb3fb306/attachment-0001.html