<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<pre class="moz-signature" cols="72">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 <i>spine</i> : 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 <i>record</i> over <i>product</i>.
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
<a class="moz-txt-link-freetext" href="http://perso.ens-lyon.fr/pierre.lescanne/">http://perso.ens-lyon.fr/pierre.lescanne/</a>
---------------------------
</pre>
</body>
</html>