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

<PRE>
String (E, C): <b>trait</b>
  % Index, substring
  <b>includes</b> <A HREF="List.html">List</A>
  <b>introduces</b> 
    __[__]: C, Int -&gt; E
    prefix: C, Int -&gt; C
    removePrefix: C, Int -&gt; C
    substring: C, Int, Int -&gt; C
  <b>asserts</b> <b>forall</b> e: E, s: C, i, n: Int
    tail(empty) == empty;
    init(empty) == empty;
    s[0] == head(s);
    n &gt;= 0 =&gt; s[n + 1] = tail(s)[n];
    prefix(empty, n) == empty;
    prefix(s, 0) == empty;
    n &gt;= 0
      =&gt; prefix(e \precat s, n + 1) = e \precat prefix(s, n);
    removePrefix(s, 0) == s;
    n &gt;= 0 
      =&gt; removePrefix(s, n + 1)
         = removePrefix(tail(s), n);
    substring(s, 0, n) == prefix(s, n);
    i &gt;= 0
      =&gt; substring(s, i + 1, n)
         = substring(tail(s), i, n)
  <b>implies</b>
    <A HREF="IndexOp.html">IndexOp</A> (\precat <b>for</b> insert)
    C <b>partitioned</b> <b>by</b> len, __[__]
    <b>converts</b> tail, init
</PRE>

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