Equations
- instCoeStringSubstring_batteries = { coe := String.toSubstring }
Returns the longest common prefix of two substrings.
The returned substring will use the same underlying string as s
.
Equations
- s.commonPrefix t = { str := s.str, startPos := s.startPos, stopPos := Substring.commonPrefix.loop s t s.startPos t.startPos }
Instances For
@[irreducible]
def
Substring.commonPrefix.loop
(s : Substring)
(t : Substring)
(spos : String.Pos)
(tpos : String.Pos)
:
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
- s.commonSuffix t = { str := s.str, startPos := Substring.commonSuffix.loop s t s.stopPos t.stopPos, stopPos := s.stopPos }
Instances For
@[irreducible]
def
Substring.commonSuffix.loop
(s : Substring)
(t : Substring)
(spos : String.Pos)
(tpos : String.Pos)
:
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
Instances For
If suff
is a suffix of s
, i.e. s = t ++ suff
, returns the remainder t
.
Equations
Instances For
s.stripPrefix pre
will remove pre
from the beginning of s
if it occurs there,
or otherwise return s
.
Equations
- s.stripPrefix pre = (Option.map Substring.toString (s.dropPrefix? pre)).getD s
Instances For
s.stripSuffix suff
will remove suff
from the end of s
if it occurs there,
or otherwise return s
.
Equations
- s.stripSuffix suff = (Option.map Substring.toString (s.dropSuffix? suff)).getD s