Nuprl Definition : radd-list
radd-list(L) == let L' ⟵ L in eval k = ||L'|| in if (k =z 0) then r0 else accelerate(k;reg-seq-list-add(L')) fi
Definitions occuring in Statement :
reg-seq-list-add: reg-seq-list-add(L),
int-to-real: r(n),
accelerate: accelerate(k;f),
length: ||as||,
callbyvalueall: callbyvalueall,
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
natural_number: $n
Definitions occuring in definition :
callbyvalueall: callbyvalueall,
callbyvalue: callbyvalue,
length: ||as||,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
int-to-real: r(n),
natural_number: $n,
accelerate: accelerate(k;f),
reg-seq-list-add: reg-seq-list-add(L)
FDL editor aliases :
radd-list
Latex:
radd-list(L) ==
let L' \mleftarrow{}{} L
in eval k = ||L'|| in
if (k =\msubz{} 0) then r0 else accelerate(k;reg-seq-list-add(L')) fi
Date html generated:
2016_05_18-AM-06_48_28
Last ObjectModification:
2015_09_23-AM-09_00_40
Theory : reals
Home
Index