Nuprl Definition : dd

For (x N), a/2N is within 1/N of x. So, if (10^n)/2,  will be the
integer that has 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 and the to place the decimal point appropriately.
(One can explode the term so displayed to see the computed x, n, and a)⋅

decimal digits of x  ==
  let answer ⟵ <"display-as", "decimal-rational", x, n, eval 10^n in eval N2 N ÷ in   N2>
  in answer

Definitions occuring in Statement :  callbyvalueall: callbyvalueall callbyvalue: callbyvalue apply: 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: a
FDL editor aliases :  dd dd

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