[Agda] Short proof of falsity

[Dan Rosén]

The natural builtins assume that you have defined naturals as in Data.Nat
in the standard library.

Best,
Dan

On Wed, Apr 18, 2012 at 5:01 PM, Anton Setzer <A.G.Setzer at swansea.ac.uk>wrote:

> > module strangeNat where
> >
> > data ℕ : Set where
> > zero : ℕ → ℕ
> > suc : ℕ → ℕ
> >
> > data ⊥ : Set where
> >
> > empty : ℕ → ⊥
> > empty (zero y) = empty y
> > empty (suc y) = empty y
> >
> > {-# BUILTIN NATURAL ℕ #-}
> >
> > p : ⊥
> > p = empty 0
>
>
> Anton and Karim
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120418/10e23963/attachment.html