Nuprl Definition : binary_map_size

binary_map_size(p) ==
  fix((λsize,p. let lbl,x = p 
                in if lbl =a "E" then 0
                   if lbl =a "T" then let key,value,cnt,left,z = x in (1 + (size left)) + (size z)
                   else 0
                   fi )) 
  p


Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  spreadn: let a,b,c,d,e = u in v[a; b; c; d; e],  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_map_size
Latex:
binary\_map\_size(p)  ==
    fix((\mlambda{}size,p.  let  lbl,x  =  p 
                                in  if  lbl  =a  "E"  then  0
                                      if  lbl  =a  "T"  then  let  key,value,cnt,left,z  =  x  in  (1  +  (size  left))  +  (size  z)
                                      else  0
                                      fi  )) 
    p


Date html generated: 2016_05_17-PM-01_37_02
Last ObjectModification: 2014_04_30-AM-11_04_34

Theory : binary-map


Home Index