Nuprl Definition : rbinop
rbinop(op;p;q) ==
if op=4
then p - q
else if op=5
then p * q
else if op=6
then (p/q)
else if op=7
then rmax(p;q)
else if op=8
then rmin(p;q)
else if op=9 then p + q else if op=10 then realexp(p;q) else (p + q)
Definitions occuring in Statement :
realexp: realexp(x;y),
rdiv: (x/y),
rmin: rmin(x;y),
rmax: rmax(x;y),
rsub: x - y,
rmul: a * b,
radd: a + b,
int_eq: if a=b then c else d,
natural_number: $n
Definitions occuring in definition :
rsub: x - y,
rmul: a * b,
rdiv: (x/y),
rmax: rmax(x;y),
rmin: rmin(x;y),
int_eq: if a=b then c else d,
natural_number: $n,
realexp: realexp(x;y),
radd: a + b
FDL editor aliases :
rbinop
Latex:
rbinop(op;p;q) ==
if op=4
then p - q
else if op=5
then p * q
else if op=6
then (p/q)
else if op=7
then rmax(p;q)
else if op=8
then rmin(p;q)
else if op=9
then p + q
else if op=10 then realexp(p;q) else (p + q)
Date html generated:
2017_10_04-PM-11_01_38
Last ObjectModification:
2017_07_03-AM-10_45_25
Theory : reals_2
Home
Index