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

<PRE>
Multiplication (N): <b>trait</b>
  % Define the operator * in terms of 0, succ, and +
  <b>includes</b>
    <A HREF="AbelianMonoid.html">AbelianMonoid</A> (* <b>for</b> \circ, 1 <b>for</b> unit, N <b>for</b> T),
    <A HREF="Addition.html">Addition</A> (N)
  <b>introduces</b>
    1: -&gt; N
    __*__: N, N -&gt; N
  <b>asserts</b> <b>forall</b> x, y: N
    1 == succ(0);
    x * 0 == 0;
    x * succ(y) == x + (x * y)
</PRE>

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