Nuprl Definition : RankEx1_size
RankEx1_size(p) ==
fix((λsize,p. let lbl,x = p
in if lbl =a "Leaf" then 0
if lbl =a "Prod" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "ProdL" then 1 + (size (snd(x)))
if lbl =a "ProdR" then 1 + (size (fst(x)))
if lbl =a "List" then 1 + Σ(size x[i] | i < ||x||)
else 0
fi ))
p
Definitions occuring in Statement :
sum: Σ(f[x] | x < k),
select: L[n],
length: ||as||,
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,
add: n + m,
natural_number: $n,
token: "$token"
FDL editor aliases :
RankEx1_size
Latex:
RankEx1\_size(p) ==
fix((\mlambda{}size,p. let lbl,x = p
in if lbl =a "Leaf" then 0
if lbl =a "Prod" then 1 + (size (fst(x))) + (size (snd(x)))
if lbl =a "ProdL" then 1 + (size (snd(x)))
if lbl =a "ProdR" then 1 + (size (fst(x)))
if lbl =a "List" then 1 + \mSigma{}(size x[i] | i < ||x||)
else 0
fi ))
p
Date html generated:
2016_05_16-AM-08_56_21
Last ObjectModification:
2014_05_06-PM-02_32_02
Theory : C-semantics
Home
Index