Nuprl Definition : dd
For a = (x N), a/2N is within 1/N of x. So, if N = (10^n)/2, a will be the
integer that has n decimal digits of x.
We actually compute <"display-as", "decimal-rational", x, n, a>
because the "display hook" will display this result as =mmm.kkkkkkk
by using the n and the a to place the decimal point appropriately.
(One can explode the term so displayed to see the computed x, n, and a)⋅
n decimal digits of x ==
let answer ⟵ <"display-as", "decimal-rational", x, n, eval N = 10^n in eval N2 = N ÷ 2 in x N2>
in answer
Definitions occuring in Statement :
callbyvalueall: callbyvalueall,
callbyvalue: callbyvalue,
apply: f a,
pair: <a, b>,
divide: n ÷ m,
natural_number: $n,
token: "$token",
fastexp: i^n
Definitions occuring in definition :
callbyvalueall: callbyvalueall,
token: "$token",
pair: <a, b>,
fastexp: i^n,
callbyvalue: callbyvalue,
divide: n ÷ m,
natural_number: $n,
apply: f a
FDL editor aliases :
dd
dd
Latex:
n decimal digits of x ==
let answer \mleftarrow{}{} <"display-as", "decimal-rational", x, n, eval N = 10\^{}n in eval N2 = N \mdiv{} 2 in x N2>
in answer
Date html generated:
2016_07_08-PM-06_30_15
Last ObjectModification:
2015_09_23-AM-09_11_24
Theory : reals
Home
Index