Nuprl Definition : pi_term_size

pi_term_size(p) ==
  fix((λsize,p. let lbl,x 
                in if lbl =a "zero" then 0
                   if lbl =a "comm" then let pre,z in (size z)
                   if lbl =a "option" then let left,right in (1 (size left)) (size right)
                   if lbl =a "par" then let left,right in (1 (size left)) (size right)
                   if lbl =a "rep" then (size x)
                   if lbl =a "new" then let name,z in (size z)
                   else 0
                   fi )) 
  p



Definitions occuring in Statement :  ifthenelse: if then else fi  eq_atom: =a y apply: a fix: fix(F) lambda: λx.A[x] spread: spread def add: m natural_number: $n token: "$token"
FDL editor aliases :  pi_term_size

Latex:
pi\_term\_size(p)  ==
    fix((\mlambda{}size,p.  let  lbl,x  =  p 
                                in  if  lbl  =a  "zero"  then  0
                                      if  lbl  =a  "comm"  then  let  pre,z  =  x  in  1  +  (size  z)
                                      if  lbl  =a  "option"  then  let  left,right  =  x  in  (1  +  (size  left))  +  (size  right)
                                      if  lbl  =a  "par"  then  let  left,right  =  x  in  (1  +  (size  left))  +  (size  right)
                                      if  lbl  =a  "rep"  then  1  +  (size  x)
                                      if  lbl  =a  "new"  then  let  name,z  =  x  in  1  +  (size  z)
                                      else  0
                                      fi  )) 
    p



Date html generated: 2015_07_23-AM-11_31_57
Last ObjectModification: 2014_05_04-PM-08_16_41

Home Index