# Documentation

## Batteries.Data.String.Basic

Equations
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
def String.dropPrefix? (s : String) (pre : Substring) :

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
def String.dropSuffix? (s : String) (suff : Substring) :

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