module Test where<br>open import Data.Nat<br><br>infixr 3 _⇨_<br>data Type : Set where<br> int : Type<br> _⇨_ : Type → Type → Type<br><br>bad : Type → ℕ<br>bad int = 0<br>bad (φ ⇨ int) = bad φ<br>bad (φ ⇨ (φ′ ⇨ φ″)) = bad (φ′ ⇨ φ″)<br>
<br>ok : Type → ℕ<br>ok int = 0<br>ok (φ ⇨ φ′) with φ′<br>... | int = ok φ<br>... | (φ″ ⇨ φ‴) = ok (φ″ ⇨ φ‴)<br><br>The problem is that function "bad" fails on termination checking. But
the function "ok" is a rewrite of "bad" that terminates.<br>Thanks. <br>Leo<br><br><div class="gmail_quote">2011/4/19 Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>></span><br>
<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">Can't see why I should not terminate. Can you provide a self-contained Agda-loadable version of your example?<br>
<br>
Thanks<br>
Andreas<div><div></div><div class="h5"><br>
<br>
On 19.04.11 1:27 AM, Leonardo Rodriguez wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;"><div><div></div><div class="h5">
Hi,<br>
<br>
This is a very simple function that fails on termination checking:<br>
<a href="http://pastebin.com/WDtSPxqq" target="_blank">http://pastebin.com/WDtSPxqq</a><br>
why ? Any hint will be appreciated<br>
thanks you in advance<br>
<br>
Leo<br>
<br>
<br>
<br></div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">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>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/%7Eabel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
</blockquote></div><br>