Nuprl Definition : decimal-digits
(d digits of x) == eval N = 10^d in eval N2 = N ÷ 2 in eval D = x N2 in eval R = D rem N in eval Q = D ÷ N in <Q, R>
Definitions occuring in Statement :
callbyvalue: callbyvalue,
apply: f a,
pair: <a, b>,
remainder: n rem m,
divide: n ÷ m,
natural_number: $n,
fastexp: i^n
Definitions occuring in definition :
fastexp: i^n,
natural_number: $n,
apply: f a,
remainder: n rem m,
callbyvalue: callbyvalue,
divide: n ÷ m,
pair: <a, b>
FDL editor aliases :
decimal-digits
decimal-digits
Latex:
(d digits of x) ==
eval N = 10\^{}d in
eval N2 = N \mdiv{} 2 in
eval D = x N2 in
eval R = D rem N in
eval Q = D \mdiv{} N in
<Q, R>
Date html generated:
2016_05_18-AM-09_28_28
Last ObjectModification:
2015_09_23-AM-09_11_17
Theory : reals
Home
Index