Nuprl Definition : binary-treeco
binary-treeco() == corec(X.lbl:Atom × if lbl =a "Leaf" then ℤ if lbl =a "Node" then left: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]
,
int: ℤ
,
token: "$token"
,
atom: Atom
,
void: Void
FDL editor aliases :
binary-treeco
binary-treeco() ==
corec(X.lbl:Atom \mtimes{} if lbl =a "Leaf" then \mBbbZ{}
if lbl =a "Node" then left:X \mtimes{} X
else Void
fi )
Date html generated:
2015_07_17-AM-07_51_27
Last ObjectModification:
2014_05_06-AM-10_17_01
Home
Index