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

<PRE>
PointwiseImage: <b>trait</b>
  % Apply elemOp to each element
  <b>assumes</b>
    <A HREF="InsertGenerated.html">InsertGenerated</A> (DE <b>for</b> E, DC <b>for</b> C),
    <A HREF="InsertGenerated.html">InsertGenerated</A> (RE <b>for</b> E, RC <b>for</b> C)
  <b>introduces</b>
    elemOp: DE -&gt; RE
    containerOp: DC -&gt; RC
  <b>asserts</b> <b>forall</b> dc: DC, de: DE
    containerOp(empty) == empty;
    containerOp(insert(de, dc)) ==
      insert(elemOp(de), containerOp(dc))
  <b>implies</b> <b>converts</b> containerOp
</PRE>

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