Nuprl Definition : l_treeco
l_treeco(L;T) ==
corec(X.lbl:Atom × if lbl =a "leaf" then L
if lbl =a "node" then val:T × left_subtree:X × X
else Void
fi )
Definitions occuring in Statement :
corec: corec(T.F[T]),
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
product: x:A × B[x],
token: "$token",
atom: Atom,
void: Void
FDL editor aliases :
l_treeco
Latex:
l\_treeco(L;T) ==
corec(X.lbl:Atom \mtimes{} if lbl =a "leaf" then L
if lbl =a "node" then val:T \mtimes{} left$_{subtree}$:X \mtimes{} X
else Void
fi )
Date html generated:
2018_05_22-PM-09_38_13
Last ObjectModification:
2014_05_05-PM-02_27_23
Theory : labeled!trees
Home
Index