[Agda] Short proof of falsity

[Ulf Norell]

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
>

The problem is that there was a missing check for BUILTIN bindings for zero
and suc
when using natural number literals. I've fixed this now so it reports a
missing builtin
thing ZERO error on the example. Thanks for spotting it.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120418/bb9eebde/attachment.html