Nuprl Definition : RankEx2

Nuprl Definition : RankEx2_size

RankEx2_size(p) ==
  fix((λ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 + Σ(size (snd(x[i])) | i < ||x||)

                   if lbl =a "UnionList" then 1 + case x of inl(a) => 0 | 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 b then t else f fi , eq_atom: x =a y, pi1: fst(t), pi2: snd(t), apply: f a, fix: fix(F), lambda: λx.A[x], spread: spread def, decide: case b of inl(x) => s[x] | inr(y) => t[y], add: n + m, natural_number: $n, token: "$token"
FDL editor aliases : RankEx2_size
RankEx2\_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_49_00 Last ObjectModification: 2014_05_06-PM-01_39_28 Home Index