Nuprl Definition : ddr
ddr(x;n) == eval N = 10^n in eval N2 = N ÷ 2 in eval a = x N2 in r(a/N)
Definitions occuring in Statement :
rat-to-real: r(a/b),
callbyvalue: callbyvalue,
apply: f a,
divide: n ÷ m,
natural_number: $n,
fastexp: i^n
Definitions occuring in definition :
fastexp: i^n,
divide: n ÷ m,
natural_number: $n,
callbyvalue: callbyvalue,
apply: f a,
rat-to-real: r(a/b)
FDL editor aliases :
ddr
Latex:
ddr(x;n) == eval N = 10\^{}n in eval N2 = N \mdiv{} 2 in eval a = x N2 in r(a/N)
Date html generated:
2016_05_18-AM-07_30_31
Last ObjectModification:
2015_09_23-AM-09_01_44
Theory : reals
Home
Index