Nuprl Definition : C_DVALUEpco

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 : sum: Σ(f[x] | x < k), select: L[n], length: ||as||, 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

Latex:
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: 2016_05_16-AM-08_48_48 Last ObjectModification: 2014_06_08-PM-03_20_26 Theory : C-semantics Home Index