[Agda] Termination-check doesn't know which case it should check?

[Darryl McAdams]

Aha! So I've just got an old version. Good to know! Thank you. :)
 
- darryl


________________________________
 From: Andrés Sicard-Ramírez <andres.sicard.ramirez at gmail.com>
To: Darryl McAdams <psygnisfive at yahoo.com> 
Cc: "agda at lists.chalmers.se" <agda at lists.chalmers.se> 
Sent: Wednesday, July 3, 2013 8:43 AM
Subject: Re: [Agda] Termination-check doesn't know which case it should check?
 

On 3 July 2013 03:34, Darryl McAdams <psygnisfive at yahoo.com> wrote:
> The following code gives a termination error on <+>-lemma even tho the
> recursion is guarded.
>
> _+>_ : ℕ → ℕ → ℕ
> zero  +> n = n
> suc m +> n = m +> suc n
>
> _<+_ : ℕ → ℕ → ℕ
> m <+ zero  = m
> m <+ suc n = suc m <+ n
>
> +>-suc-lemma : (m n : ℕ) → m +> suc n ≡ suc (m +> n)
> +>-suc-lemma m n = {!!}
>
> <+-suc-lemma : (m n : ℕ) → suc m <+ n ≡ suc (m <+ n)
> <+-suc-lemma m n = {!!}
>
> <+>-lemma : (m n : ℕ) → m +> n ≡ m <+ n
> <+>-lemma 0       0 = refl
> <+>-lemma 0       (suc n) rewrite <+-suc-lemma 0 n | cong suc (<+>-lemma 0
> n) = refl
> <+>-lemma (suc m) 0       rewrite +>-suc-lemma m 0 | cong suc (<+>-lemma m
> 0) = refl
> <+>-lemma (suc m) (suc n) rewrite <+-suc-lemma (suc m) n | <+-suc-lemma m n
>                                 | +>-suc-lemma m (suc n) | +>-suc-lemma m n
>                                 | cong (suc ∘ suc) (<+>-lemma m n) = refl
>

I couldn't reproduce the issue with Agda-2.3.2.1.

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130703/254c18cf/attachment.html