Documentation

Batteries.Data.String.Basic

theorem String.Pos.ne_zero_of_lt {a : String.Pos} {b : String.Pos} :
a < bb 0

Returns the longest common prefix of two substrings. The returned substring will use the same underlying string as s.

Equations
Instances For
    @[irreducible]

    Returns the ending position of the common prefix, working up from spos, tpos.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Returns the longest common suffix of two substrings. The returned substring will use the same underlying string as s.

      Equations
      Instances For
        @[irreducible]

        Returns the starting position of the common prefix, working down from spos, tpos.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          If pre is a prefix of s, i.e. s = pre ++ t, returns the remainder t.

          Equations
          • s.dropPrefix? pre = let t := s.commonPrefix pre; if t.bsize = pre.bsize then some { str := s.str, startPos := t.stopPos, stopPos := s.stopPos } else none
          Instances For

            If suff is a suffix of s, i.e. s = t ++ suff, returns the remainder t.

            Equations
            • s.dropSuffix? suff = let t := s.commonSuffix suff; if t.bsize = suff.bsize then some { str := s.str, startPos := s.startPos, stopPos := t.startPos } else none
            Instances For

              If pre is a prefix of s, i.e. s = pre ++ t, returns the remainder t.

              Equations
              • s.dropPrefix? pre = s.toSubstring.dropPrefix? pre
              Instances For

                If suff is a suffix of s, i.e. s = t ++ suff, returns the remainder t.

                Equations
                • s.dropSuffix? suff = s.toSubstring.dropSuffix? suff
                Instances For

                  s.stripPrefix pre will remove pre from the beginning of s if it occurs there, or otherwise return s.

                  Equations
                  Instances For

                    s.stripSuffix suff will remove suff from the end of s if it occurs there, or otherwise return s.

                    Equations
                    Instances For
                      def String.count (s : String) (c : Char) :

                      Count the occurrences of a character in a string.

                      Equations
                      Instances For