<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span>Aha! So I've just got an old version. Good to know! Thank you. :)</span></div><div></div><div> </div><div>- darryl<br></div> <div style="font-family: arial, helvetica, sans-serif; font-size: 10pt; "> <div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "> <div dir="ltr"> <hr size="1"> <font size="2" face="Arial"> <b><span style="font-weight:bold;">From:</span></b> Andrés Sicard-Ramírez <andres.sicard.ramirez@gmail.com><br> <b><span style="font-weight: bold;">To:</span></b> Darryl McAdams <psygnisfive@yahoo.com> <br><b><span style="font-weight: bold;">Cc:</span></b> "agda@lists.chalmers.se" <agda@lists.chalmers.se> <br> <b><span style="font-weight: bold;">Sent:</span></b> Wednesday, July 3, 2013 8:43 AM<br> <b><span style="font-weight: bold;">Subject:</span></b> Re:
[Agda] Termination-check doesn't know which case it should check?<br> </font> </div> <div class="y_msg_container"><br>On 3 July 2013 03:34, Darryl McAdams <<a ymailto="mailto:psygnisfive@yahoo.com" href="mailto:psygnisfive@yahoo.com">psygnisfive@yahoo.com</a>> wrote:<br>> The following code gives a termination error on <+>-lemma even tho the<br>> recursion is guarded.<br>><br>> _+>_ : ℕ → ℕ → ℕ<br>> zero +> n = n<br>> suc m +> n = m +> suc n<br>><br>> _<+_ : ℕ → ℕ → ℕ<br>> m <+ zero = m<br>> m <+ suc n = suc m <+ n<br>><br>> +>-suc-lemma : (m n : ℕ) → m +> suc n ≡ suc (m +> n)<br>> +>-suc-lemma m n = {!!}<br>><br>> <+-suc-lemma : (m n : ℕ) → suc m <+ n ≡ suc (m <+ n)<br>> <+-suc-lemma m n = {!!}<br>><br>> <+>-lemma : (m n : ℕ) → m +> n ≡ m <+ n<br>> <+>-lemma 0
0 = refl<br>> <+>-lemma 0 (suc n) rewrite <+-suc-lemma 0 n | cong suc (<+>-lemma 0<br>> n) = refl<br>> <+>-lemma (suc m) 0 rewrite +>-suc-lemma m 0 | cong suc (<+>-lemma m<br>> 0) = refl<br>> <+>-lemma (suc m) (suc n) rewrite <+-suc-lemma (suc m) n | <+-suc-lemma m n<br>> | +>-suc-lemma m (suc n) | +>-suc-lemma m n<br>> | cong (suc ∘ suc) (<+>-lemma m n) = refl<br>><br><br>I couldn't reproduce the issue with Agda-2.3.2.1.<br><br>-- <br>Andrés<br><br></div> </div> </div> </div></body></html>