Nuprl Definition : binary-tree_size
binary-tree_size(p) ==
  fix((λsize,p. let lbl,x = p 
                in if lbl =a "Leaf" then 0
                   if lbl =a "Node" then let left,right = x in (1 + (size left)) + (size right)
                   else 0
                   fi )) 
  p
Definitions occuring in Statement : 
ifthenelse: if b then t else f fi 
, 
eq_atom: x =a y
, 
apply: f a
, 
fix: fix(F)
, 
lambda: λx.A[x]
, 
spread: spread def, 
add: n + m
, 
natural_number: $n
, 
token: "$token"
FDL editor aliases : 
binary-tree_size
binary-tree\_size(p)  ==
    fix((\mlambda{}size,p.  let  lbl,x  =  p 
                                in  if  lbl  =a  "Leaf"  then  0
                                      if  lbl  =a  "Node"  then  let  left,right  =  x  in  (1  +  (size  left))  +  (size  right)
                                      else  0
                                      fi  )) 
    p
Date html generated:
2015_07_17-AM-07_51_41
Last ObjectModification:
2014_05_06-AM-10_17_44
Home
Index