instance instCoeStringSubstring_batteries : Coe String Substring

Equations

• instCoeStringSubstring_batteries = { coe := String.toSubstring }

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

def Substring.commonPrefix (s : Substring) (t : Substring) : Substring

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 }

@[irreducible]

def Substring.commonPrefix.loop (s : Substring) (t : Substring) (spos : String.Pos) (tpos : String.Pos) : 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.

def Substring.commonSuffix (s : Substring) (t : Substring) : Substring

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 }

@[irreducible]

def Substring.commonSuffix.loop (s : Substring) (t : Substring) (spos : String.Pos) (tpos : String.Pos) : 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.

def Substring.dropPrefix? (s : Substring) (pre : Substring) : Option Substring

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

Equations

• s.dropPrefix? pre = if (s.commonPrefix pre).bsize = pre.bsize then some { str := s.str, startPos := (s.commonPrefix pre).stopPos, stopPos := s.stopPos } else none

def Substring.dropSuffix? (s : Substring) (suff : Substring) : Option Substring

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

Equations

• s.dropSuffix? suff = if (s.commonSuffix suff).bsize = suff.bsize then some { str := s.str, startPos := s.startPos, stopPos := (s.commonSuffix suff).startPos } else none

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

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

def String.stripPrefix (s : String) (pre : Substring) : String

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

def String.stripSuffix (s : String) (suff : Substring) : String

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

def String.count (s : String) (c : Char) : Nat

Count the occurrences of a character in a string.

Equations

• s.count c = String.foldl (fun (n : Nat) (d : Char) => if d = c then n + 1 else n) 0 s

def String.toAsciiByteArray (s : String) : ByteArray

Convert a string of assumed-ASCII characters into a byte array. (If any characters are non-ASCII they will be reduced modulo 256.)

Note: if you just need the underlying ByteArray of a non-ASCII string, use String.toUTF8.

Equations

• s.toAsciiByteArray = String.toAsciiByteArray.loop s 0 ByteArray.empty

@[irreducible]

def String.toAsciiByteArray.loop (s : String) (p : String.Pos) (out : ByteArray) : ByteArray

Internal implementation of toAsciiByteArray. loop p out = out ++ toAsciiByteArray ({ s with startPos := p } : Substring)

Equations

• String.toAsciiByteArray.loop s p out = if h : s.atEnd p = true then out else let c := s.get p; let_fun this := ⋯; String.toAsciiByteArray.loop s (s.next p) (out.push c.toUInt8)