Nuprl Definition : ratadd

ratadd(x;y) ==
  let a,b = x 
  in let c,d = y 
     in eval g = better-gcd(b;d) in
        eval b' = b ÷ g in
        eval d' = d ÷ g in
        eval a' = (d' * a) + (b' * c) in
        eval d'' = b' * d in
          <a', d''>


Definitions occuring in Statement :  better-gcd: better-gcd(a;b),  callbyvalue: callbyvalue,  spread: spread def,  pair: <a, b>,  divide: n ÷ m,  multiply: n * m,  add: n + m
Definitions occuring in definition :  spread: spread def,  better-gcd: better-gcd(a;b),  divide: n ÷ m,  add: n + m,  callbyvalue: callbyvalue,  multiply: n * m,  pair: <a, b>
FDL editor aliases :  ratadd
Latex:
ratadd(x;y)  ==
    let  a,b  =  x 
    in  let  c,d  =  y 
          in  eval  g  =  better-gcd(b;d)  in
                eval  b'  =  b  \mdiv{}  g  in
                eval  d'  =  d  \mdiv{}  g  in
                eval  a'  =  (d'  *  a)  +  (b'  *  c)  in
                eval  d''  =  b'  *  d  in
                    <a',  d''>


Date html generated: 2019_10_30-AM-09_17_29
Last ObjectModification: 2019_01_10-PM-02_45_59

Theory : reals


Home Index