Nuprl Definition : RankEx4_size

RankEx4_size(p) ==
  fix((λsize,p. let lbl,x in if lbl =a "Foo" then case of inl(a) => inr(b) => size else 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 decide: case of inl(x) => s[x] inr(y) => t[y] add: m natural_number: $n token: "$token"
FDL editor aliases :  RankEx4_size
RankEx4\_size(p)  ==
    fix((\mlambda{}size,p.  let  lbl,x  =  p 
                                in  if  lbl  =a  "Foo"  then  1  +  case  x  of  inl(a)  =>  0  |  inr(b)  =>  size  b  else  0  fi  )) 

Date html generated: 2015_07_17-AM-07_50_53
Last ObjectModification: 2014_05_06-AM-11_45_11

Home Index