[Agda] a tutorial for proof by coinduction

[Pierre Lescanne (en)]

I have a specific question.  Here are two formalisations of coinductive binary trees

mutual
   record BT (A : Set) : Set where
     coinductive
     field
       u : A ⊎ Node A
       
   record Node (A : Set) : Set where
     coinductive
     field
       ↙ ↘ : BT A

record BT' (A : Set) : Set where
   coinductive
   field
     node : A ⊎ (BT' A × BT' A )

open BT
open Node
open BT'

-------------
Now I define three objects/spine/  : one is in BT and two are in BT'.  Those in BT' are not accepted, I suspect that this is due to the termination checker, which prefers/record/  over/product/.
Am I right ? Or am I mistaking ?
-------------

mutual
   spine : BT ℕ
   spine = record {u = inj₂ spineN}
   
   spineN : Node ℕ
   ↙ spineN = spine
   ↘ spineN = record{u = inj₁ 0}

mutual
   spine' : BT' ℕ
   spine' = record {node = inj₂ (spine'' , record{node = inj₁ 0})}
   
   spine'' : BT' ℕ
   spine'' = record {node = inj₂ (spine' , record{node = inj₁ 0})}

spine₀ : BT' ℕ
spine₀ = record {node = inj₂ (spine₀ , record{node = inj₁ 0})}



-- 
Regards,

---------------------------
Pierre Lescanne (Emeritus Professor)
LIP / École normale supérieure de Lyon
46 allée d'Italie
69364 LYON Cedex 07, France
tél: +33 6 85 70 94 31
http://perso.ens-lyon.fr/pierre.lescanne/
---------------------------

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200114/b015b92b/attachment.html>