Nuprl Definition : RankEx2co_size
RankEx2co_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 :
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