[<A HREF="Rational.ps">PostScript</A>]

<PRE>
Rational: <b>trait</b>
  % For use in the trait FloatingPoint.
  <b>includes</b>
    <A HREF="Exponentiation.html">Exponentiation</A> (Q <b>for</b> T, P <b>for</b> N),
    <A HREF="IntegerAndPositive.html">IntegerAndPositive</A> (Int, P),
    <A HREF="MinMax.html">MinMax</A> (Q),
    <A HREF="TotalOrder.html">TotalOrder</A> (Q)
  <b>introduces</b>
    __/__: Int, P -&gt; Q
    0, 1: -&gt; Q
    -__, __\inv, abs: Q -&gt; Q
    __+__, __*__, __-__, __/__: Q, Q -&gt; Q
  <b>asserts</b>
    Q <b>generated</b> <b>by</b> __/__:Int,P-&gt;Q
    <b>forall</b> i, i1, i2: Int, p, p1, p2, p3: P, q, q1, q2: Q
      0/p == 0;
      int(p)/p == 1;
      i1/p1 = i2/p2 == i1 * int(p2) = i2 * int(p1);
      -(i/p) == (-i)/p;
      (int(p1)/p2)\inv == int(p2)/p1;
      (-q)\inv == -(q\inv);
      abs(i/p) == abs(i)/p;
      (i1/p) + (i2/p) == (i1 + i2)/p;
      (i1/p1) * (i2/p2) == (i1 * i2)/(p1 * p2);
      q1 - q2 == q1 + (-q2);
      q1/q2 == q1 * (q2\inv);
      (i1/p) &lt; (i2/p) == i1 &lt; i2
  <b>implies</b>
    <A HREF="AC.html">AC</A> (+, Q),
    <A HREF="AC.html">AC</A> (*, Q),
    <A HREF="Field.html">Field</A> (Q <b>for</b> T)
    <b>forall</b> i, i1, i2: Int, p, p1, p2, p3: P, q: Q
      q + 0 == q;
      -q == 0 - q;
      (i1/p) - (i2/p) == (i1 - i2)/p;
      q * 0 == 0;
      q * 1 == q;
      q\inv == 1/q;
      (i/p1)/(int(p2)/p3) == (i * int(p3))/(p1 * p2)
  <b>converts</b>
      0:-&gt;Q, 1:-&gt;Q, -:Q -&gt;Q, \inv, abs:Q -&gt;Q,
      +:Q,Q-&gt;Q, -:Q,Q-&gt;Q, *:Q,Q-&gt;Q, /:Q,Q-&gt;Q,
      **:Q,P-&gt;Q, min:Q,Q-&gt;Q, max:Q,Q-&gt;Q,
      &lt;:Q,Q-&gt;Bool, &gt;:Q,Q-&gt;Bool,
      &lt;=:Q,Q-&gt;Bool, &gt;=:Q,Q-&gt;Bool
    exempting 0\inv
</PRE>

[<A HREF="toc.html">Table of Contents</A>] [<A HREF="index.html">Index</A>]