[Agda] Termination checking with Lexicographic recursive calls

[Nils Anders Danielsson]

On 2020-02-17 19:03, Sergey Goncharov wrote:
> Any ideas why the following is not accepted?

> h₁ (suc n) (suc k) p rewrite +-suc (π′ n + suc n) k with (π₁⁻¹ (π′ n + suc n + k)) | inspect π₁⁻¹ (π′ n + suc n + k)
> h₁ (suc n) (suc k) p | zero  | [ eq ] = ⊥-elim (1+n≰n (≤-trans (m∸n≡0⇒m≤n {suc n} {k} (trans (sym (h₁ (suc n) k (≤-trans (n≤1+n k) p))) eq)) (≤-pred p)))

Auxiliary functions are generated when you use rewrite or with. In this
case the auxiliary functions get n and k as arguments, and then you call
h₁ with suc n as one of the arguments.

Your code is not self-contained, but I suspect that you can make it work
by using --termination-depth=2.

-- 
/NAD