[Agda] question about termination checker

[Nils Anders Danielsson]

On 01/10/2019 16.58, selinger at mathstat.dal.ca wrote:
> lemma2 : Nat -> Nat
> lemma2 zero = zero
> lemma2 (succ zero) = zero
> lemma2 (succ (succ x)) = ih
>    where
>    ih = lemma2 (succ x)

This is expanded to something like the following code:

   mutual

     ih : Nat -> Nat
     ih x = lemma2 (succ x)

     lemma2 : Nat -> Nat
     lemma2 zero = zero
     lemma2 (succ zero) = zero
     lemma2 (succ (succ x)) = ih x

The termination checker accepts your code if you use
--termination-depth=2.

-- 
/NAD