Nuprl Definition : rounding-div
[b ÷ m] ==
eval n = m in
eval a = b in
let q,r = divrem(a; n)
in eval r2 = 2 * r in
if (r2) < (n) then if (-n) < (r2) then q else (q - 1) else (q + 1)
Definitions occuring in Statement :
callbyvalue: callbyvalue,
less: if (a) < (b) then c else d,
spread: spread def,
divrem: divrem(n; m),
multiply: n * m,
subtract: n - m,
add: n + m,
minus: -n,
natural_number: $n
Definitions occuring in definition :
spread: spread def,
callbyvalue: callbyvalue,
multiply: n * m,
less: if (a) < (b) then c else d,
minus: -n,
subtract: n - m,
add: n + m,
natural_number: $n
FDL editor aliases :
rounding-div
Latex:
[b \mdiv{} m] ==
eval n = m in
eval a = b in
let q,r = divrem(a; n)
in eval r2 = 2 * r in
if (r2) < (n) then if (-n) < (r2) then q else (q - 1) else (q + 1)
Date html generated:
2019_06_20-PM-01_13_27
Last ObjectModification:
2019_02_18-PM-02_43_40
Theory : int_2
Home
Index