<p>Thanks Guillaume, it works :-)</p>
<div class="gmail_quote">Le 23 juin 2012 17:03, "gallais @ <a href="http://ensl.org">ensl.org</a>" <<a href="mailto:guillaume.allais@ens-lyon.org">guillaume.allais@ens-lyon.org</a>> 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 <<a href="mailto:guillaume.brunerie@gmail.com">guillaume.brunerie@gmail.com</a>> wrote:<br>
> Hi,<br>
> I have the following code<br>
><br>
>> module Test where<br>
>><br>
>> data ℕ : Set where<br>
>> O : ℕ<br>
>> S : ℕ → ℕ<br>
>><br>
>> -- Does compile<br>
>> g : ℕ → ℕ<br>
>> g O = O<br>
>> g (S O) = S O<br>
>> g (S (S n)) = g (S n)<br>
>><br>
>> -- Does not compile<br>
>> f : ℕ → ℕ<br>
>> f O = O<br>
>> f (S O) = S O<br>
>> f (S (S n)) = a where<br>
>> a : ℕ<br>
>> a = f (S n)<br>
><br>
> Why does g compiles and not f (f is highlighted red in emacs)?<br>
> Is this a bug or something not yet implemented?<br>
> Is there an easy way to work around it?<br>
> (I using a dev version of Agda compiled a few weeks ago)<br>
><br>
> Thanks!<br>
><br>
> Guillaume<br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>