<br>The natural builtins assume that you have defined naturals as in Data.Nat in the standard library.<br><br>Best,<br>Dan<br><br><div class="gmail_quote">On Wed, Apr 18, 2012 at 5:01 PM, Anton Setzer <span dir="ltr"><<a href="mailto:A.G.Setzer@swansea.ac.uk">A.G.Setzer@swansea.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">> module strangeNat where<br>
><br>
> data ℕ : Set where<br>
> zero : ℕ → ℕ<br>
> suc : ℕ → ℕ<br>
><br>
> data ⊥ : Set where<br>
><br>
> empty : ℕ → ⊥<br>
> empty (zero y) = empty y<br>
> empty (suc y) = empty y<br>
><br>
> {-# BUILTIN NATURAL ℕ #-}<br>
><br>
> p : ⊥<br>
> p = empty 0<br>
<br>
<br>
Anton and Karim<br>
</blockquote></div><br>