Nuprl Definition : qrng
<ℚ+*> ==
<ℚ, λx,y. qeq(x;y), λx,y. q_le(x;y), λx,y. (x + y), 0, λx.-(x), λx,y. (x * y), 1, λx,y. if qeq(y;0) then inr ⋅ else i\000Cnl (x/y) fi >
Definitions occuring in Statement :
q_le: q_le(r;s),
qdiv: (r/s),
qmul: r * s,
qadd: r + s,
rationals: ℚ,
qeq: qeq(r;s),
ifthenelse: if b then t else f fi ,
it: ⋅,
lambda: λx.A[x],
pair: <a, b>,
inr: inr x ,
inl: inl x,
minus: -n,
natural_number: $n
Definitions occuring in definition :
rationals: ℚ,
q_le: q_le(r;s),
qadd: r + s,
minus: -n,
qmul: r * s,
pair: <a, b>,
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
qeq: qeq(r;s),
natural_number: $n,
inr: inr x ,
it: ⋅,
inl: inl x,
qdiv: (r/s)
FDL editor aliases :
qrng
Latex:
<\mBbbQ{}+*> ==
<\mBbbQ{}
, \mlambda{}x,y. qeq(x;y)
, \mlambda{}x,y. q\_le(x;y)
, \mlambda{}x,y. (x + y)
, 0
, \mlambda{}x.-(x)
, \mlambda{}x,y. (x * y)
, 1
, \mlambda{}x,y. if qeq(y;0) then inr \mcdot{} else inl (x/y) fi >
Date html generated:
2016_05_15-PM-10_43_23
Last ObjectModification:
2015_09_23-AM-08_27_16
Theory : rationals
Home
Index