<br><div class="gmail_quote">On Wed, Apr 18, 2012 at 5:01 PM, Anton Setzer <span dir="ltr">&lt;<a href="mailto:A.G.Setzer@swansea.ac.uk">A.G.Setzer@swansea.ac.uk</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

&gt; module strangeNat where<br>
&gt;<br>
&gt; data ℕ : Set where<br>
&gt; zero : ℕ → ℕ<br>
&gt; suc : ℕ → ℕ<br>
&gt;<br>
&gt; data ⊥ : Set where<br>
&gt;<br>
&gt; empty : ℕ → ⊥<br>
&gt; empty (zero y) = empty y<br>
&gt; empty (suc y) = empty y<br>
&gt;<br>
&gt; {-# BUILTIN NATURAL ℕ #-}<br>
&gt;<br>
&gt; p : ⊥<br>
&gt; p = empty 0<br></blockquote><div><br></div><div>The problem is that there was a missing check for BUILTIN bindings for zero and suc</div><div>when using natural number literals. I&#39;ve fixed this now so it reports a missing builtin</div>

<div>thing ZERO error on the example. Thanks for spotting it.</div><div><br></div><div>/ Ulf</div></div>