<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;">
Hi Leonardo,<br>
<br>
That should really terminate, I fixed this in the darcs version of Agda now.<div class="im"><br></div></blockquote><div>Thank you :D <br></div><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<div class="im">
<br>
On 19.04.11 8:12 PM, Leonardo Rodriguez wrote:<br>
<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
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>
</blockquote>
<br></div>
What you can also do is an overlapping clause here:<br>
<br>
bad (φ ⇨ φ′) = bad φ′<br><br></blockquote><div><br>The "bad" function is an example for reveal the problem. I had this problem with another<br>function where i can't overlap clauses. <br></div><div><br> </div>
<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
This termination checks even in the release version.<br>
<br></blockquote><div>Thank you again :D <br></div><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
Cheers,<br><font color="#888888">
Andreas</font><div><div></div><div class="h5"><br>
<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>
</div></div></blockquote></div><br>