Nuprl Definition : bs_treeco
bs_treeco(E) ==
corec(X.lbl:Atom × if lbl =a "null" then Unit
if lbl =a "leaf" then E
if lbl =a "node" then left:X × value:E × 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,
unit: Unit,
product: x:A × B[x],
token: "$token",
atom: Atom,
void: Void
Definitions occuring in definition :
corec: corec(T.F[T]),
atom: Atom,
unit: Unit,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
token: "$token",
product: x:A × B[x],
void: Void
FDL editor aliases :
bs_treeco
Latex:
bs\_treeco(E) ==
corec(X.lbl:Atom \mtimes{} if lbl =a "null" then Unit
if lbl =a "leaf" then E
if lbl =a "node" then left:X \mtimes{} value:E \mtimes{} X
else Void
fi )
Date html generated:
2016_05_15-PM-01_50_02
Last ObjectModification:
2016_04_07-PM-02_24_08
Theory : tree_1
Home
Index