Nuprl Definition : qadd
r + s ==
let r' ⟵ r
in let s' ⟵ s
in if isint(r')
then if isint(s') then r' + s' else let i,j = s' in <(r' * j) + i, j> fi
else let p,q = r'
in if isint(s') then <p + (s' * q), q> else let i,j = s' in <(p * j) + (i * q), q * j> fi
fi
Definitions occuring in Statement :
callbyvalueall: callbyvalueall,
ifthenelse: if b then t else f fi ,
bfalse: ff,
btrue: tt,
isint: isint def,
spread: spread def,
pair: <a, b>,
multiply: n * m,
add: 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,
pair: <a, b>,
add: n + m,
multiply: n * m
FDL editor aliases :
qadd
Latex:
r + s ==
let r' \mleftarrow{}{} r
in let s' \mleftarrow{}{} s
in if isint(r')
then if isint(s') then r' + s' else let i,j = s' in <(r' * j) + i, j> fi
else let p,q = r'
in if isint(s') then <p + (s' * q), q> else let i,j = s' in <(p * j) + (i * q), q * j> fi
fi
Date html generated:
2016_05_15-PM-10_37_30
Last ObjectModification:
2015_09_23-AM-08_26_53
Theory : rationals
Home
Index