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

<PRE>
IntegerAndPositive (Int, P): <b>trait</b>
  % Conversions between Int's and P's
  <b>includes</b>
    <A HREF="Integer.html">Integer</A> (Int),
    <A HREF="Positive.html">Positive</A> (P)
  <b>introduces</b>
    int: P -&gt; Int
    pos: Int -&gt; P
  <b>asserts</b> <b>forall</b> p: P
    int(1) == 1;
    int(succ(p)) == succ(int(p));
    pos(int(p)) == p
</PRE>

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