Nuprl Definition : RankEx2co_size

RankEx2co_size(p) ==
  fix((λsize,p. let lbl,x 
                in if lbl =a "LeafT" then 0
                   if lbl =a "LeafS" then 0
                   if lbl =a "Prod" then (size (fst(fst(x))))
                   if lbl =a "Union" then case of inl(a) => size (snd(a)) inr(b) => size b
                   if lbl =a "ListProd" then + Σ(size (snd(x[i])) i < ||x||)
                   if lbl =a "UnionList" then case of inl(a) => inr(b) => Σ(size b[i] i < ||b||)
                   else 0
                   fi )) 
  p



Definitions occuring in Statement :  select: L[n] length: ||as|| sum: Σ(f[x] x < k) ifthenelse: if then else fi  eq_atom: =a y pi1: fst(t) pi2: snd(t) 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 :  RankEx2co_size
RankEx2co\_size(p)  ==
    fix((\mlambda{}size,p.  let  lbl,x  =  p 
                                in  if  lbl  =a  "LeafT"  then  0
                                      if  lbl  =a  "LeafS"  then  0
                                      if  lbl  =a  "Prod"  then  1  +  (size  (fst(fst(x))))
                                      if  lbl  =a  "Union"  then  1  +  case  x  of  inl(a)  =>  size  (snd(a))  |  inr(b)  =>  size  b
                                      if  lbl  =a  "ListProd"  then  1  +  \mSigma{}(size  (snd(x[i]))  |  i  <  ||x||)
                                      if  lbl  =a  "UnionList"
                                          then  1  +  case  x  of  inl(a)  =>  0  |  inr(b)  =>  \mSigma{}(size  b[i]  |  i  <  ||b||)
                                      else  0
                                      fi  )) 
    p



Date html generated: 2015_07_17-AM-07_48_53
Last ObjectModification: 2014_05_06-PM-01_38_30

Home Index