Nuprl Definition : qeq
qeq(r;s) ==
let r' ⟵ r
in let s' ⟵ s
in if isint(r')
then if isint(s') then (r' =z s') else let i,j = s' in (r' * j =z i) fi
else let p,q = r'
in if isint(s') then (p =z s' * q) else let i,j = s' in (p * j =z i * q) fi
fi
Definitions occuring in Statement :
callbyvalueall: callbyvalueall,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
bfalse: ff,
btrue: tt,
isint: isint def,
spread: spread def,
multiply: n * m
Definitions occuring in definition :
callbyvalueall: callbyvalueall,
ifthenelse: if b then t else f fi ,
isint: isint def,
btrue: tt,
bfalse: ff,
spread: spread def,
eq_int: (i =z j),
multiply: n * m
FDL editor aliases :
qeq
Latex:
qeq(r;s) ==
let r' \mleftarrow{}{} r
in let s' \mleftarrow{}{} s
in if isint(r')
then if isint(s') then (r' =\msubz{} s') else let i,j = s' in (r' * j =\msubz{} i) fi
else let p,q = r'
in if isint(s') then (p =\msubz{} s' * q) else let i,j = s' in (p * j =\msubz{} i * q) fi
fi
Date html generated:
2016_05_15-PM-10_36_30
Last ObjectModification:
2015_09_23-AM-08_26_50
Theory : rationals
Home
Index