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

<PRE>
PairwiseExtension (\circ, \odot, E, C): <b>trait</b>
  % Induce a binary operator on containers
  % from a binary operator on elements.
  <b>assumes</b> <A HREF="Container.html">Container</A> (E, C)
  <b>introduces</b>
    __\circ __: E, E -&gt; E
    __\odot __: C, C -&gt; C
  <b>asserts</b> <b>forall</b> e1, e2: E, c1, c2: C
    empty \odot empty == empty;
    (c1 \neq empty /\ c2 \neq empty)
      =&gt; c1 \odot c2 = insert(head(c1) \circ head(c2),
                           tail(c1) \odot tail(c2));
  <b>implies</b> <b>converts</b> \odot
    exempting <b>forall</b> e: E, c: C
      empty \odot insert(e, c), insert(e, c) \odot empty
</PRE>

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