Nuprl Definition : rP_to_real
rP_to_real(stack;L)
==r if L = Ax then stack otherwise let op,more = L
in if op=1
then let c,evenmore = more
in rP_to_real([r(c) / stack];evenmore)
else if op=2
then let c,d,evenmore = more in
rP_to_real([r(c) + (r(d))/10^num-digits(d) / stack];evenmore)
else if op=3
then rP_to_real(<4 * MachinPi4(), stack>;more)
else if op <z 11
then let q,p,s = stack in
rP_to_real([rbinop(op;p;q) / s];more)
if op <z 25
then let p,s = stack
in rP_to_real([runop(op - 11;p) / s];more)
if op <z 29
then let c,evenmore = more
in let p,s = stack
in let q = if op=25
then rroot(c;p)
else if op=26
then c * p
else if op=27 then (p)/c else p^c in
rP_to_real([q / s];evenmore)
else stack
fi
rP_to_real(stack;L) ==
fix((λrP_to_real,stack,L. if L = Ax then stack otherwise let op,more = L
in if op=1
then let c,evenmore = more
in rP_to_real [r(c) / stack] evenmore
else if op=2
then let c,d,evenmore = more in
rP_to_real
[r(c) + (r(d))/10^num-digits(d) / stack]
evenmore
else if op=3
then rP_to_real <4 * MachinPi4(), stack> more
else if op <z 11
then let q,p,s = stack in
rP_to_real [rbinop(op;p;q) / s] more
if op <z 25
then let p,s = stack
in rP_to_real
[runop(op - 11;p) / s]
more
if op <z 29
then let c,evenmore = more
in let p,s = stack
in let q = if op=25
then rroot(c;p)
else if op=26
then c * p
else if op=27
then (p)/c
else p^c in
rP_to_real [q / s]
evenmore
else stack
fi ))
stack
L
Definitions occuring in Statement :
runop: runop(op;p),
rbinop: rbinop(op;p;q),
num-digits: num-digits(k),
MachinPi4: MachinPi4(),
rroot: rroot(i;x),
rnexp: x^k1,
int-rdiv: (a)/k1,
int-rmul: k1 * a,
radd: a + b,
int-to-real: r(n),
fastexp: i^n,
cons: [a / b],
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
let: let,
spreadn: spread3,
isaxiom: if z = Ax then a otherwise b,
int_eq: if a=b then c else d,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
isaxiom: if z = Ax then a otherwise b,
radd: a + b,
int-to-real: r(n),
fastexp: i^n,
num-digits: num-digits(k),
pair: <a, b>,
MachinPi4: MachinPi4(),
spreadn: spread3,
rbinop: rbinop(op;p;q),
runop: runop(op;p),
subtract: n - m,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
spread: spread def,
let: let,
rroot: rroot(i;x),
int-rmul: k1 * a,
int_eq: if a=b then c else d,
natural_number: $n,
int-rdiv: (a)/k1,
rnexp: x^k1,
apply: f a,
cons: [a / b]
FDL editor aliases :
rP_to_real
Latex:
rP\_to\_real(stack;L)
==r if L = Ax then stack otherwise let op,more = L
in if op=1
then let c,evenmore = more
in rP\_to\_real([r(c) / stack];evenmore)
else if op=2
then let c,d,evenmore = more in
rP\_to\_real([r(c) + (r(d))/10\^{}num-digits(d) /
stack];evenmore)
else if op=3
then rP\_to\_real(ɜ * MachinPi4(), stack>more)
else if op <z 11
then let q,p,s = stack in
rP\_to\_real([rbinop(op;p;q) / s];more)
if op <z 25
then let p,s = stack
in rP\_to\_real([runop(op - 11;p) /
s];more)
if op <z 29
then let c,evenmore = more
in let p,s = stack
in let q = if op=25
then rroot(c;p)
else if op=26
then c * p
else if op=27
then (p)/c
else p\^{}c in
rP\_to\_real([q / s];evenmore)
else stack
fi
Latex:
rP\_to\_real(stack;L) ==
fix((\mlambda{}rP\_to$_{real}$,stack,L. if L = Ax then stack
otherwise let op,more = L
in if op=1
then let c,evenmore = more
in rP\_to$_{real}$ [r(c) / stack] ev\000Cenmore
else if op=2
then let c,d,evenmore = more in
rP\_to$_{real}$
[r(c) + (r(d))/10\^{}num-digits(d) / stack]
evenmore
else if op=3
then rP\_to$_{real}$ ɜ * Machi\000CnPi4(), stack> more
else if op <z 11
then let q,p,s = stack in
rP\_to$_{real}$ [rb\000Cinop(op;p;q) / s] more
if op <z 25
then let p,s = stack
in rP\_to$_{real}$ \000C[runop(op - 11;p) / s]
more
if op <z 29
then let c,evenmore = more
in let p,s = stack
in let q = if op=25
then rroot(c;p)
else if op=26
then c * p
else if op=27
then (p)/c
else p\^{}c in
rP\_to$_{real\mbackslash{}ff7\000Cd$ [q / s] evenmore
else stack
fi ))
stack
L
Date html generated:
2018_05_22-PM-03_08_37
Last ObjectModification:
2017_11_27-PM-00_05_14
Theory : reals_2
Home
Index