Nuprl Definition : C_DVALUEpco_size
C_DVALUEpco_size(p) ==
fix((λsize,p. let lbl,x = p
in if lbl =a "Null" then 0
if lbl =a "Int" then 0
if lbl =a "Pointer" then 0
if lbl =a "Array"
then 1
+ Σ(size ((snd(snd(x))) ((fst(x)) + i)) | i < if fst(x) ≤z fst(snd(x))
then (fst(snd(x))) - fst(x)
else 0
fi )
if lbl =a "Struct" then 1 + Σ(size ((snd(x)) fst(x)[a]) | a < ||fst(x)||)
else 0
fi ))
p
Definitions occuring in Statement :
select: L[n]
,
length: ||as||
,
sum: Σ(f[x] | x < k)
,
le_int: i ≤z j
,
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,
subtract: n - m
,
add: n + m
,
natural_number: $n
,
token: "$token"
FDL editor aliases :
C_DVALUEpco_size
C\_DVALUEpco\_size(p) ==
fix((\mlambda{}size,p. let lbl,x = p
in if lbl =a "Null" then 0
if lbl =a "Int" then 0
if lbl =a "Pointer" then 0
if lbl =a "Array"
then 1
+ \mSigma{}(size ((snd(snd(x))) ((fst(x)) + i)) | i < if fst(x) \mleq{}z fst(snd(x))
then (fst(snd(x))) - fst(x)
else 0
fi )
if lbl =a "Struct" then 1 + \mSigma{}(size ((snd(x)) fst(x)[a]) | a < ||fst(x)||)
else 0
fi ))
p
Date html generated:
2015_07_17-AM-07_43_59
Last ObjectModification:
2014_06_08-PM-03_20_26
Home
Index