Nuprl Definition : decimal-digits

(d digits of x) ==  eval 10^d in eval N2 N ÷ in eval N2 in eval rem in eval D ÷ in   <Q, R>

Definitions occuring in Statement :  callbyvalue: callbyvalue apply: a pair: <a, b> remainder: rem m divide: n ÷ m natural_number: $n fastexp: i^n
Definitions occuring in definition :  fastexp: i^n natural_number: $n apply: a remainder: rem m callbyvalue: callbyvalue divide: n ÷ m pair: <a, b>
FDL editor aliases :  decimal-digits decimal-digits

(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