[Agda] Termination checking with Lexicographic recursive calls

[Sergey Goncharov]

>     Perhaps we are using different versions of the standard library. I'm
>     using the branch called "experimental".
> 
> 
> Looking at the code, I can't see why it shouldn't work on experimental? 
> What's the error you're getting Nils?
> 

Ah, it is my bad, I forgot to include the definitions of π₁⁻¹ and π₂⁻¹ :

------------------------------------
π₁⁻¹ π₂⁻¹ : ℕ → ℕ

π₁⁻¹ 0 = 0
π₁⁻¹ (suc n) with (π₁⁻¹ n)
π₁⁻¹ (suc n) | zero = suc (π₂⁻¹ n)
π₁⁻¹ (suc n) | suc m = m

π₂⁻¹ 0 = 0
π₂⁻¹ (suc n) with (π₁⁻¹ n)
π₂⁻¹ (suc n) | zero  = 0
π₂⁻¹ (suc n) | suc _ = suc (π₂⁻¹ n).

------------------------------------

These form the inverse of the Cantor pairing function.. Sorry for that.

Sergey

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5384 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200219/9000c351/attachment.p7s>