Nuprl Definition : qmul
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' * i, j> fi 
     else let p,q = r' 
          in if isint(s') then <p * s', q> else let i,j = s' in <p * i, 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
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>
, 
multiply: n * m
FDL editor aliases : 
qmul
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'  *  i,  j>  fi 
          else  let  p,q  =  r' 
                    in  if  isint(s')  then  <p  *  s',  q>  else  let  i,j  =  s'  in  <p  *  i,  q  *  j>  fi 
          fi 
Date html generated:
2016_05_15-PM-10_37_40
Last ObjectModification:
2015_09_23-AM-08_26_53
Theory : rationals
Home
Index