Nuprl Definition : real_exp
real_exp(x) ==
case rless-case((r1)/5;(r1)/4;42;x)
of inl(_) =>
eval N = canonical-bound(|4 * x|) in
rexp-small((x)/N)^N
| inr(_) =>
case rless-case((r(-1))/4;(r(-1))/5;42;x)
of inl(_) =>
rexp-small(x)
| inr(_) =>
eval N = canonical-bound(|4 * x|) in
rexp-small((x)/N)^N
Definitions occuring in Statement :
rexp-small: rexp-small(x),
rless-case: rless-case(x;y;n;z),
rabs: |x|,
rnexp: x^k1,
int-rdiv: (a)/k1,
int-rmul: k1 * a,
canonical-bound: canonical-bound(r),
int-to-real: r(n),
callbyvalue: callbyvalue,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
minus: -n,
natural_number: $n
Definitions occuring in definition :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
rless-case: rless-case(x;y;n;z),
int-to-real: r(n),
minus: -n,
callbyvalue: callbyvalue,
canonical-bound: canonical-bound(r),
rabs: |x|,
int-rmul: k1 * a,
natural_number: $n,
rnexp: x^k1,
rexp-small: rexp-small(x),
int-rdiv: (a)/k1
FDL editor aliases :
real_exp
Latex:
real\_exp(x) ==
case rless-case((r1)/5;(r1)/4;42;x)
of inl($_{}$) =>
eval N = canonical-bound(|4 * x|) in
rexp-small((x)/N)\^{}N
| inr($_{}$) =>
case rless-case((r(-1))/4;(r(-1))/5;42;x)
of inl($_{}$) =>
rexp-small(x)
| inr($_{}$) =>
eval N = canonical-bound(|4 * x|) in
rexp-small((x)/N)\^{}N
Date html generated:
2019_10_30-AM-11_41_12
Last ObjectModification:
2019_02_04-AM-11_38_32
Theory : reals_2
Home
Index