<p>Thanks Guillaume, it works :-)</p>
<div class="gmail_quote">Le 23 juin 2012 17:03, &quot;gallais @ <a href="http://ensl.org">ensl.org</a>&quot; &lt;<a href="mailto:guillaume.allais@ens-lyon.org">guillaume.allais@ens-lyon.org</a>&gt; a écrit :<br type="attribution">
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Guillaume,<br>
<br>
you can ask agda to do more work during termination analysis<br>
with the appropriate pragma. Cf the release notes for 2.2.8 [1]<br>
(ctrl+f termination-depth to find quickly the interesting bits)<br>
<br>
Using {-# OPTIONS --termination-depth=2 #-} solves your problem.<br>
<br>
Cheers,<br>
<br>
--<br>
gallais<br>
<br>
[1] <a href="http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Version-2-2-8" target="_blank">http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Version-2-2-8</a><br>
<br>
On 23 June 2012 15:54, Guillaume Brunerie &lt;<a href="mailto:guillaume.brunerie@gmail.com">guillaume.brunerie@gmail.com</a>&gt; wrote:<br>
&gt; Hi,<br>
&gt; I have the following code<br>
&gt;<br>
&gt;&gt; module Test where<br>
&gt;&gt;<br>
&gt;&gt; data ℕ : Set where<br>
&gt;&gt;   O : ℕ<br>
&gt;&gt;   S : ℕ → ℕ<br>
&gt;&gt;<br>
&gt;&gt; -- Does compile<br>
&gt;&gt; g : ℕ → ℕ<br>
&gt;&gt; g O = O<br>
&gt;&gt; g (S O) = S O<br>
&gt;&gt; g (S (S n)) = g (S n)<br>
&gt;&gt;<br>
&gt;&gt; -- Does not compile<br>
&gt;&gt; f : ℕ → ℕ<br>
&gt;&gt; f O = O<br>
&gt;&gt; f (S O) = S O<br>
&gt;&gt; f (S (S n)) = a where<br>
&gt;&gt;   a : ℕ<br>
&gt;&gt;   a = f (S n)<br>
&gt;<br>
&gt; Why does g compiles and not f (f is highlighted red in emacs)?<br>
&gt; Is this a bug or something not yet implemented?<br>
&gt; Is there an easy way to work around it?<br>
&gt; (I using a dev version of Agda compiled a few weeks ago)<br>
&gt;<br>
&gt; Thanks!<br>
&gt;<br>
&gt; Guillaume<br>
&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>