Nuprl Definition : pi_term

Nuprl Definition : pi_term_size

pi_term_size(p) ==
  fix((λ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

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 : 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