Nuprl Definition : MultiTreeco
MultiTreeco(T) ==
corec(X.lbl:Atom × if lbl =a "Node" then labels:{L:Atom List| 0 < ||L||} × ({a:Atom| (a ∈ labels)} ─→ X)
if lbl =a "Leaf" then T
else Void
fi )
Definitions occuring in Statement :
l_member: (x ∈ l),
length: ||as||,
list: T List,
corec: corec(T.F[T]),
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
less_than: a < b,
set: {x:A| B[x]} ,
function: x:A ─→ B[x],
product: x:A × B[x],
natural_number: $n,
token: "$token",
atom: Atom,
void: Void
FDL editor aliases :
MultiTreeco
MultiTreeco(T) ==
corec(X.lbl:Atom \mtimes{} if lbl =a "Node" then labels:\{L:Atom List| 0 < ||L||\} \mtimes{} (\{a:Atom| (a \mmember{} labels)\000C\} {}\mrightarrow{} X)
if lbl =a "Leaf" then T
else Void
fi )
Date html generated:
2015_07_17-AM-07_45_33
Last ObjectModification:
2014_06_10-PM-03_27_39
Home
Index