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