Nuprl Definition : rsum
Σ{x[k] | n≤k≤m} == eval n' = n in eval m' = m in let xs ⟵ map(λk.x[k];[n', m' + 1)) in radd-list(xs)
Definitions occuring in Statement :
radd-list: radd-list(L),
from-upto: [n, m),
map: map(f;as),
callbyvalueall: callbyvalueall,
callbyvalue: callbyvalue,
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
callbyvalue: callbyvalue,
callbyvalueall: callbyvalueall,
map: map(f;as),
lambda: λx.A[x],
from-upto: [n, m),
add: n + m,
natural_number: $n,
radd-list: radd-list(L)
FDL editor aliases :
rsum
rsum
Latex:
\mSigma{}\{x[k] | n\mleq{}k\mleq{}m\} ==
eval n' = n in
eval m' = m in
let xs \mleftarrow{}{} map(\mlambda{}k.x[k];[n', m' + 1))
in radd-list(xs)
Date html generated:
2016_05_18-AM-07_41_30
Last ObjectModification:
2015_09_23-AM-09_02_32
Theory : reals
Home
Index