Nuprl Definition : truncate-rational
truncate-rational(q;e) == case q_less(e;1) of inl() => eval b = rat-int-bound((1/e)) in <integer-part(q * b), b> | inr(\000C) => integer-part(q)
Definitions occuring in Statement :
integer-part: integer-part(q),
rat-int-bound: rat-int-bound(q),
q_less: q_less(r;s),
qdiv: (r/s),
qmul: r * s,
callbyvalue: callbyvalue,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
natural_number: $n
Definitions occuring in definition :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
q_less: q_less(r;s),
callbyvalue: callbyvalue,
rat-int-bound: rat-int-bound(q),
qdiv: (r/s),
natural_number: $n,
pair: <a, b>,
qmul: r * s,
integer-part: integer-part(q)
FDL editor aliases :
truncate-rational
Latex:
truncate-rational(q;e) ==
case q\_less(e;1) of inl() => eval b = rat-int-bound((1/e)) in <integer-part(q * b), b> | inr() => \000Cinteger-part(q)
Date html generated:
2016_05_15-PM-11_42_58
Last ObjectModification:
2015_09_23-AM-08_31_20
Theory : rationals
Home
Index