Nuprl Definition : l_tree_size
l_tree_size(p) ==
fix((λsize,p. let lbl,x = p
in if lbl =a "leaf" then 0
if lbl =a "node" then let val,left_subtree,z = x in (1 + (size left_subtree)) + (size z)
else 0
fi ))
p
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
spreadn: spread3,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
add: n + m,
natural_number: $n,
token: "$token"
FDL editor aliases :
l_tree_size
l\_tree\_size(p) ==
fix((\mlambda{}size,p. let lbl,x = p
in if lbl =a "leaf" then 0
if lbl =a "node"
then let val,left$_{subtree}$,z = x in
(1 + (size left$_{subtree}$)) + (size z)
else 0
fi ))
p
Date html generated:
2015_07_17-AM-07_41_22
Last ObjectModification:
2014_05_05-PM-02_27_52
Home
Index