Nuprl Definition : rat-int-part

rat-int-part(q) ==
  if q is an integer then <q, 0>
  else let n,m = q
       in eval a = n ÷ m in
          eval b = n rem m in
            if (b =_z 0) then <a, 0>
            if 0 <z m then if 0 ≤z n then <a, (b/m)> else <a - 1, (b + m/m)> fi
            if 0 ≤z n then <a - 1, (b + m/m)>
            else <a, (b/m)>
            fi

Definitions occuring in Statement : qdiv: (r/s), le_int: i ≤z j, callbyvalue: callbyvalue, ifthenelse: if b then t else f fi , lt_int: i <z j, eq_int: (i =_z j), isint: isint def, spread: spread def, pair: <a, b>, remainder: n rem m, divide: n ÷ m, subtract: n - m, add: n + m, natural_number: $n
Definitions occuring in definition : isint: isint def, spread: spread def, divide: n ÷ m, callbyvalue: callbyvalue, remainder: n rem m, eq_int: (i =_z j), lt_int: i <z j, ifthenelse: if b then t else f fi , le_int: i ≤z j, subtract: n - m, natural_number: $n, add: n + m, pair: <a, b>, qdiv: (r/s)
FDL editor aliases : rat-int-part

Latex:
rat-int-part(q) == if q is an integer then <q, 0> else let n,m = q in eval a = n \mdiv{} m in eval b = n rem m in if (b =\msubz{} 0) then <a, 0> if 0 <z m then if 0 \mleq{}z n then <a, (b/m)> else <a - 1, (b + m/m)> fi if 0 \mleq{}z n then <a - 1, (b + m/m)> else <a, (b/m)> fi Date html generated: 2016_05_15-PM-11_33_41 Last ObjectModification: 2015_09_23-AM-08_30_07 Theory : rationals Home Index