def List.asString (s : List Char) : String

Creates a string that contains the characters in a list, in order.

Examples:

• ['L', '∃', '∀', 'N'].asString = "L∃∀N"
• [].asString = ""
• ['a', 'a', 'a'].asString = "aaa"

Equations

• s.asString = { data := s }

instance String.instOfNatPos : OfNat Pos 0

Equations

• String.instOfNatPos = { ofNat := { } }

instance String.instLT : LT String

Equations

• String.instLT = { lt := fun (s₁ s₂ : String) => s₁.data < s₂.data }

@[extern lean_string_dec_lt]

instance String.decidableLT (s₁ s₂ : String) : Decidable (s₁ < s₂)

Equations

• s₁.decidableLT s₂ = s₁.data.decidableLT s₂.data

@[reducible, inline, deprecated String.decidableLT (since := "2024-12-13")]

abbrev String.decLt (s₁ s₂ : String) : Decidable (s₁ < s₂)

Equations

• String.decLt = String.decidableLT

@[reducible]

def String.le (a b : String) : Prop

Non-strict inequality on strings, typically used via the ≤ operator.

a ≤ b is defined to mean ¬ b < a.

Equations

• a.le b = ¬b < a

instance String.instLE : LE String

Equations

• String.instLE = { le := String.le }

instance String.decLE (s₁ s₂ : String) : Decidable (s₁ ≤ s₂)

Equations

• s₁.decLE s₂ = inferInstanceAs (Decidable ¬s₂ < s₁)

@[extern lean_string_length]

def String.length : String → Nat

Returns the length of a string in Unicode code points.

Examples:

• "".length = 0
• "abc".length = 3
• "L∃∀N".length = 4

Equations

• { data := s }.length = s.length

@[extern lean_string_push]

def String.push : String → Char → String

Adds a character to the end of a string.

The internal implementation uses dynamic arrays and will perform destructive updates if the string is not shared.

Examples:

• "abc".push 'd' = "abcd"
• "".push 'a' = "a"

Equations

• { data := s }.push x✝ = { data := s ++ [x✝] }

@[extern lean_string_append]

def String.append : String → String → String

Appends two strings. Usually accessed via the ++ operator.

The internal implementation will perform destructive updates if the string is not shared.

Examples:

• "abc".append "def" = "abcdef"
• "abc" ++ "def" = "abcdef"
• "" ++ "" = ""

Equations

• { data := a }.append { data := b } = { data := a ++ b }

def String.toList (s : String) : List Char

Converts a string to a list of characters.

Even though the logical model of strings is as a structure that wraps a list of characters, this operation takes time and space linear in the length of the string. At runtime, strings are represented as dynamic arrays of bytes.

Examples:

• "abc".toList = ['a', 'b', 'c']
• "".toList = []
• "\n".toList = ['\n']

Equations

• s.toList = s.data

@[extern lean_string_is_valid_pos]

def String.Pos.isValid (s : String) (p : Pos) : Bool

Returns true if p is a valid UTF-8 position in the string s.

This means that p ≤ s.endPos and p lies on a UTF-8 character boundary. At runtime, this operation takes constant time.

Examples:

• String.Pos.isValid "abc" ⟨0⟩ = true
• String.Pos.isValid "abc" ⟨1⟩ = true
• String.Pos.isValid "abc" ⟨3⟩ = true
• String.Pos.isValid "abc" ⟨4⟩ = false
• String.Pos.isValid "𝒫(A)" ⟨0⟩ = true
• String.Pos.isValid "𝒫(A)" ⟨1⟩ = false
• String.Pos.isValid "𝒫(A)" ⟨2⟩ = false
• String.Pos.isValid "𝒫(A)" ⟨3⟩ = false
• String.Pos.isValid "𝒫(A)" ⟨4⟩ = true

Equations

• String.Pos.isValid s p = String.Pos.isValid.go p s.data 0

def String.Pos.isValid.go (p : Pos) : List Char → Pos → Bool

Equations

• String.Pos.isValid.go p [] x✝ = decide (x✝ = p)
• String.Pos.isValid.go p (c :: cs) x✝ = if x✝ = p then true else String.Pos.isValid.go p cs (x✝ + c)

def String.utf8GetAux : List Char → Pos → Pos → Char

Equations

• String.utf8GetAux [] x✝¹ x✝ = default
• String.utf8GetAux (c :: cs) x✝¹ x✝ = if x✝¹ = x✝ then c else String.utf8GetAux cs (x✝¹ + c) x✝

@[extern lean_string_utf8_get]

def String.get (s : String) (p : Pos) : Char

Returns the character at position p of a string. If p is not a valid position, returns the fallback value (default : Char), which is 'A', but does not panic.

This function is overridden with an efficient implementation in runtime code. See String.utf8GetAux for the reference implementation.

Examples:

• "abc".get ⟨1⟩ = 'b'
• "abc".get ⟨3⟩ = (default : Char) because byte 3 is at the end of the string.
• "L∃∀N".get ⟨2⟩ = (default : Char) because byte 2 is in the middle of '∃'.

Equations

• { data := s_1 }.get p = String.utf8GetAux s_1 0 p

def String.utf8GetAux? : List Char → Pos → Pos → Option Char

Equations

• String.utf8GetAux? [] x✝¹ x✝ = none
• String.utf8GetAux? (c :: cs) x✝¹ x✝ = if x✝¹ = x✝ then some c else String.utf8GetAux? cs (x✝¹ + c) x✝

@[extern lean_string_utf8_get_opt]

def String.get? : String → Pos → Option Char

Returns the character at position p of a string. If p is not a valid position, returns none.

This function is overridden with an efficient implementation in runtime code. See String.utf8GetAux? for the reference implementation.

Examples:

• "abc".get? ⟨1⟩ = some 'b'
• "abc".get? ⟨3⟩ = none
• "L∃∀N".get? ⟨1⟩ = some '∃'
• "L∃∀N".get? ⟨2⟩ = none

Equations

• { data := s }.get? x✝ = String.utf8GetAux? s 0 x✝

@[extern lean_string_utf8_get_bang]

def String.get! (s : String) (p : Pos) : Char

Returns the character at position p of a string. Panics if p is not a valid position.

See String.get? for a safer alternative.

This function is overridden with an efficient implementation in runtime code. See String.utf8GetAux for the reference implementation.

Examples

• "abc".get! ⟨1⟩ = 'b'

Equations

• { data := s_1 }.get! p = String.utf8GetAux s_1 0 p

def String.utf8SetAux (c' : Char) : List Char → Pos → Pos → List Char

Equations

• String.utf8SetAux c' [] x✝¹ x✝ = []
• String.utf8SetAux c' (c :: cs) x✝¹ x✝ = if x✝¹ = x✝ then c' :: cs else c :: String.utf8SetAux c' cs (x✝¹ + c) x✝

@[extern lean_string_utf8_set]

def String.set : String → Pos → Char → String

Replaces the character at a specified position in a string with a new character. If the position is invalid, the string is returned unchanged.

If both the replacement character and the replaced character are 7-bit ASCII characters and the string is not shared, then it is updated in-place and not copied.

Examples:

• "abc".set ⟨1⟩ 'B' = "aBc"
• "abc".set ⟨3⟩ 'D' = "abc"
• "L∃∀N".set ⟨4⟩ 'X' = "L∃XN"
• "L∃∀N".set ⟨2⟩ 'X' = "L∃∀N" because '∃' is a multi-byte character, so the byte index 2 is an invalid position.

Equations

• { data := s }.set x✝¹ x✝ = { data := String.utf8SetAux x✝ s 0 x✝¹ }

def String.modify (s : String) (i : Pos) (f : Char → Char) : String

Replaces the character at position p in the string s with the result of applying f to that character. If p is an invalid position, the string is returned unchanged.

If both the replacement character and the replaced character are 7-bit ASCII characters and the string is not shared, then it is updated in-place and not copied.

Examples:

• abc.modify ⟨1⟩ Char.toUpper = "aBc"
• abc.modify ⟨3⟩ Char.toUpper = "abc"

Equations

• s.modify i f = s.set i (f (s.get i))

@[extern lean_string_utf8_next]

def String.next (s : String) (p : Pos) : Pos

Returns the next position in a string after position p. The result is unspecified if p is not a valid position or if p = s.endPos.

A run-time bounds check is performed to determine whether p is at the end of the string. If a bounds check has already been performed, use String.next' to avoid a repeated check.

Some examples where the result is unspecified:

• "abc".next ⟨3⟩, since 3 = "abc".endPos
• "L∃∀N".next ⟨2⟩, since 2 points into the middle of a multi-byte UTF-8 character

Examples:

• "abc".get ("abc".next 0) = 'b'
• "L∃∀N".get (0 |> "L∃∀N".next |> "L∃∀N".next) = '∀'

Equations

• s.next p = p + s.get p

def String.utf8PrevAux : List Char → Pos → Pos → Pos

Equations

• String.utf8PrevAux [] x✝¹ x✝ = 0
• String.utf8PrevAux (c :: cs) x✝¹ x✝ = if x✝¹ + c = x✝ then x✝¹ else String.utf8PrevAux cs (x✝¹ + c) x✝

@[extern lean_string_utf8_prev]

def String.prev : String → Pos → Pos

Returns the position in a string before a specified position, p. If p = ⟨0⟩, returns 0. If p is not a valid position, the result is unspecified.

For example, "L∃∀N".prev ⟨3⟩ is unspecified, since byte 3 occurs in the middle of the multi-byte character '∃'.

Examples:

• "abc".get ("abc".endPos |> "abc".prev) = 'c'
• "L∃∀N".get ("L∃∀N".endPos |> "L∃∀N".prev |> "L∃∀N".prev |> "L∃∀N".prev) = '∃'

Equations

• { data := s }.prev x✝ = if x✝ = 0 then 0 else String.utf8PrevAux s 0 x✝

@[inline]

def String.front (s : String) : Char

Returns the first character in s. If s = "", returns (default : Char).

Examples:

• "abc".front = 'a'
• "".front = (default : Char)

Equations

• s.front = s.get 0

@[inline]

def String.back (s : String) : Char

Returns the last character in s. If s = "", returns (default : Char).

Examples:

• "abc".back = 'c'
• "".back = (default : Char)

Equations

• s.back = s.get (s.prev s.endPos)

@[extern lean_string_utf8_at_end]

def String.atEnd : String → Pos → Bool

Returns true if a specified byte position is greater than or equal to the position which points to the end of a string. Otherwise, returns false.

Examples:

• (0 |> "abc".next |> "abc".next |> "abc".atEnd) = false
• (0 |> "abc".next |> "abc".next |> "abc".next |> "abc".next |> "abc".atEnd) = true
• (0 |> "L∃∀N".next |> "L∃∀N".next |> "L∃∀N".next |> "L∃∀N".atEnd) = false
• (0 |> "L∃∀N".next |> "L∃∀N".next |> "L∃∀N".next |> "L∃∀N".next |> "L∃∀N".atEnd) = true
• "abc".atEnd ⟨4⟩ = true
• "L∃∀N".atEnd ⟨7⟩ = false
• "L∃∀N".atEnd ⟨8⟩ = true

Equations

• x✝¹.atEnd x✝ = decide (x✝.byteIdx ≥ x✝¹.utf8ByteSize)

@[extern lean_string_utf8_get_fast]

def String.get' (s : String) (p : Pos) (h : ¬s.atEnd p = true) : Char

Returns the character at position p of a string. Returns (default : Char), which is 'A', if p is not a valid position.

Requires evidence, h, that p is within bounds instead of performing a run-time bounds check as in String.get.

A typical pattern combines get' with a dependent if-expression to avoid the overhead of an additional bounds check. For example:

def getInBounds? (s : String) (p : String.Pos) : Option Char :=
  if h : s.atEnd p then none else some (s.get' p h)

Even with evidence of ¬ s.atEnd p, p may be invalid if a byte index points into the middle of a multi-byte UTF-8 character. For example, "L∃∀N".get' ⟨2⟩ (by decide) = (default : Char).

Examples:

• "abc".get' 0 (by decide) = 'a'
• let lean := "L∃∀N"; lean.get' (0 |> lean.next |> lean.next) (by decide) = '∀'

Equations

• { data := s_2 }.get' p h_2 = String.utf8GetAux s_2 0 p

@[extern lean_string_utf8_next_fast]

def String.next' (s : String) (p : Pos) (h : ¬s.atEnd p = true) : Pos

Returns the next position in a string after position p. The result is unspecified if p is not a valid position.

Requires evidence, h, that p is within bounds. No run-time bounds check is performed, as in String.next.

A typical pattern combines String.next' with a dependent if-expression to avoid the overhead of an additional bounds check. For example:

def next? (s: String) (p : String.Pos) : Option Char :=
  if h : s.atEnd p then none else s.get (s.next' p h)

Example:

• let abc := "abc"; abc.get (abc.next' 0 (by decide)) = 'b'

Equations

• s.next' p h = p + s.get p

theorem Char.utf8Size_pos (c : Char) : 0 < c.utf8Size

theorem Char.utf8Size_le_four (c : Char) : c.utf8Size ≤ 4

@[reducible, inline, deprecated Char.utf8Size_pos (since := "2026-06-04")]

abbrev String.one_le_csize (c : Char) : 0 < c.utf8Size

Equations

• String.one_le_csize = Char.utf8Size_pos

@[simp]

theorem String.pos_lt_eq (p₁ p₂ : Pos) : (p₁ < p₂) = (p₁.byteIdx < p₂.byteIdx)

@[simp]

theorem String.pos_add_char (p : Pos) (c : Char) : (p + c).byteIdx = p.byteIdx + c.utf8Size

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

theorem String.lt_next (s : String) (i : Pos) : i.byteIdx < (s.next i).byteIdx

theorem String.utf8PrevAux_lt_of_pos (cs : List Char) (i p : Pos) : p ≠ 0 → (utf8PrevAux cs i p).byteIdx < p.byteIdx

theorem String.prev_lt_of_pos (s : String) (i : Pos) (h : i ≠ 0) : (s.prev i).byteIdx < i.byteIdx

@[irreducible]

def String.posOfAux (s : String) (c : Char) (stopPos pos : Pos) : Pos

Equations

• s.posOfAux c stopPos pos = if h : pos < stopPos then if (s.get pos == c) = true then pos else let_fun this := ⋯; s.posOfAux c stopPos (s.next pos) else pos

@[inline]

def String.posOf (s : String) (c : Char) : Pos

Returns the position of the first occurrence of a character, c, in a string s. If s does not contain c, returns s.endPos.

Examples:

• "abcba".posOf 'a' = ⟨0⟩
• "abcba".posOf 'z' = ⟨5⟩
• "L∃∀N".posOf '∀' = ⟨4⟩

Equations

• s.posOf c = s.posOfAux c s.endPos 0

@[irreducible]

def String.revPosOfAux (s : String) (c : Char) (pos : Pos) : Option Pos

Equations

• s.revPosOfAux c pos = if h : pos = 0 then none else let_fun this := ⋯; let pos := s.prev pos; if (s.get pos == c) = true then some pos else s.revPosOfAux c pos

@[inline]

def String.revPosOf (s : String) (c : Char) : Option Pos

Returns the position of the last occurrence of a character, c, in a string s. If s does not contain c, returns none.

Examples:

• "abcabc".refPosOf 'a' = some ⟨3⟩
• "abcabc".revPosOf 'z' = none
• "L∃∀N".revPosOf '∀' = some ⟨4⟩

Equations

• s.revPosOf c = s.revPosOfAux c s.endPos

@[irreducible]

def String.findAux (s : String) (p : Char → Bool) (stopPos pos : Pos) : Pos

Equations

• s.findAux p stopPos pos = if h : pos < stopPos then if p (s.get pos) = true then pos else let_fun this := ⋯; s.findAux p stopPos (s.next pos) else pos

@[inline]

def String.find (s : String) (p : Char → Bool) : Pos

Finds the position of the first character in a string for which the Boolean predicate p returns true. If there is no such character in the string, then the end position of the string is returned.

Examples:

• "coffee tea water".find (·.isWhitespace) = ⟨6⟩
• "tea".find (· == 'X') = ⟨3⟩
• "".find (· == 'X') = ⟨0⟩

Equations

• s.find p = s.findAux p s.endPos 0

@[irreducible]

def String.revFindAux (s : String) (p : Char → Bool) (pos : Pos) : Option Pos

Equations

• s.revFindAux p pos = if h : pos = 0 then none else let_fun this := ⋯; let pos := s.prev pos; if p (s.get pos) = true then some pos else s.revFindAux p pos

@[inline]

def String.revFind (s : String) (p : Char → Bool) : Option Pos

Finds the position of the last character in a string for which the Boolean predicate p returns true. If there is no such character in the string, then none is returned.

Examples:

• "coffee tea water".revFind (·.isWhitespace) = some ⟨10⟩
• "tea".revFind (· == 'X') = none
• "".revFind (· == 'X') = none

Equations

• s.revFind p = s.revFindAux p s.endPos

@[reducible, inline]

abbrev String.Pos.min (p₁ p₂ : Pos) : Pos

Returns either p₁ or p₂, whichever has the least byte index.

Equations

• p₁.min p₂ = { byteIdx := p₁.byteIdx.min p₂.byteIdx }

def String.firstDiffPos (a b : String) : Pos

Returns the first position where the two strings differ.

If one string is a prefix of the other, then the returned position is the end position of the shorter string. If the strings are identical, then their end position is returned.

Examples:

• "tea".firstDiffPos "ten" = ⟨2⟩
• "tea".firstDiffPos "tea" = ⟨3⟩
• "tea".firstDiffPos "teas" = ⟨3⟩
• "teas".firstDiffPos "tea" = ⟨3⟩

Equations

• a.firstDiffPos b = String.firstDiffPos.loop a b (a.endPos.min b.endPos) 0

@[irreducible]

def String.firstDiffPos.loop (a b : String) (stopPos i : Pos) : Pos

Equations

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

@[extern lean_string_utf8_extract]

def String.extract : String → Pos → Pos → String

Creates a new string that consists of the region of the input string delimited by the two positions.

The result is "" if the start position is greater than or equal to the end position or if the start position is at the end of the string. If either position is invalid (that is, if either points at the middle of a multi-byte UTF-8 character) then the result is unspecified.

Examples:

• "red green blue".extract ⟨0⟩ ⟨3⟩ = "red"
• "red green blue".extract ⟨3⟩ ⟨0⟩ = ""
• "red green blue".extract ⟨0⟩ ⟨100⟩ = "red green blue"
• "red green blue".extract ⟨4⟩ ⟨100⟩ = "green blue"
• "L∃∀N".extract ⟨2⟩ ⟨100⟩ = "green blue"

Equations

• { data := s }.extract x✝¹ x✝ = if x✝¹.byteIdx ≥ x✝.byteIdx then "" else { data := String.extract.go₁ s 0 x✝¹ x✝ }

def String.extract.go₁ : List Char → Pos → Pos → Pos → List Char

Equations

• String.extract.go₁ [] x✝² x✝¹ x✝ = []
• String.extract.go₁ (c :: cs) x✝² x✝¹ x✝ = if x✝² = x✝¹ then String.extract.go₂ (c :: cs) x✝² x✝ else String.extract.go₁ cs (x✝² + c) x✝¹ x✝

def String.extract.go₂ : List Char → Pos → Pos → List Char

Equations

• String.extract.go₂ [] x✝¹ x✝ = []
• String.extract.go₂ (c :: cs) x✝¹ x✝ = if x✝¹ = x✝ then [] else c :: String.extract.go₂ cs (x✝¹ + c) x✝

@[irreducible, specialize #[]]

def String.splitAux (s : String) (p : Char → Bool) (b i : Pos) (r : List String) : List String

Equations

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

@[specialize #[]]

def String.split (s : String) (p : Char → Bool) : List String

Splits a string at each character for which p returns true.

The characters that satisfy p are not included in any of the resulting strings. If multiple characters in a row satisfy p, then the resulting list will contain empty strings.

Examples:

• "coffee tea water".split (·.isWhitespace) = ["coffee", "tea", "water"]
• "coffee tea water".split (·.isWhitespace) = ["coffee", "", "tea", "", "water"]
• "fun x =>\n x + 1\n".split (· == '\n') = ["fun x =>", " x + 1", ""]

Equations

• s.split p = s.splitAux p 0 0 []

@[irreducible]

def String.splitOnAux (s sep : String) (b i j : Pos) (r : List String) : List String

Auxiliary for splitOn. Preconditions:

• sep is not empty
• b <= i are indexes into s
• j is an index into sep, and not at the end

It represents the state where we have currently parsed some split parts into r (in reverse order), b is the beginning of the string / the end of the previous match of sep, and the first j bytes of sep match the bytes i-j .. i of s.

Equations

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

@[inline]

def String.splitOn (s : String) (sep : String := " ") : List String

Splits a string s on occurrences of the separator string sep. The default separator is " ".

When sep is empty, the result is [s]. When sep occurs in overlapping patterns, the first match is taken. There will always be exactly n+1 elements in the returned list if there were n non-overlapping matches of sep in the string. The separators are not included in the returned substrings.

Examples:

• "here is some text ".splitOn = ["here", "is", "some", "text", ""]
• "here is some text ".splitOn "some" = ["here is ", " text "]
• "here is some text ".splitOn "" = ["here is some text "]
• "ababacabac".splitOn "aba" = ["", "bac", "c"]

Equations

• s.splitOn sep = if (sep == "") = true then [s] else s.splitOnAux sep 0 0 0 []

instance String.instInhabited : Inhabited String

Equations

• String.instInhabited = { default := "" }

instance String.instAppend : Append String

Equations

• String.instAppend = { append := String.append }

@[inline]

def String.pushn (s : String) (c : Char) (n : Nat) : String

Adds multiple repetitions of a character to the end of a string.

Returns s, with n repetitions of c at the end. Internally, the implementation repeatedly calls String.push, so the string is modified in-place if there is a unique reference to it.

Examples:

• "indeed".pushn '!' 2 = "indeed!!"
• "indeed".pushn '!' 0 = "indeed"
• "".pushn ' ' 4 = " "

Equations

• s.pushn c n = Nat.repeat (fun (s : String) => s.push c) n s

@[inline]

def String.isEmpty (s : String) : Bool

Checks whether a string is empty.

Empty strings are equal to "" and have length and end position 0.

Examples:

• "".isEmpty = true
• "empty".isEmpty = false
• " ".isEmpty = false

Equations

• s.isEmpty = (s.endPos == 0)

@[inline]

def String.join (l : List String) : String

Appends all the strings in a list of strings, in order.

Use String.intercalate to place a separator string between the strings in a list.

Examples:

• String.join ["gr", "ee", "n"] = "green"
• String.join ["b", "", "l", "", "ue"] = "red"
• String.join [] = ""

Equations

• String.join l = List.foldl (fun (r s : String) => r ++ s) "" l

@[inline]

def String.singleton (c : Char) : String

Returns a new string that contains only the character c.

Because strings are encoded in UTF-8, the resulting string may take multiple bytes.

Examples:

• String.singleton 'L' = "L"
• String.singleton ' ' = " "
• String.singleton '"' = "\""
• String.singleton '𝒫' = "𝒫"

Equations

• String.singleton c = "".push c

def String.intercalate (s : String) : List String → String

Appends the strings in a list of strings, placing the separator s between each pair.

Examples:

• ", ".intercalate ["red", "green", "blue"] = "red, green, blue"
• " and ".intercalate ["tea", "coffee"] = "tea and coffee"
• " | ".intercalate ["M", "", "N"] = "M | | N"

Equations

• s.intercalate [] = ""
• s.intercalate (a :: as) = String.intercalate.go a s as

def String.intercalate.go (acc s : String) : List String → String

Equations

• String.intercalate.go acc s (a :: as) = String.intercalate.go (acc ++ s ++ a) s as
• String.intercalate.go acc s [] = acc

structure String.Iterator : Type

An iterator over the characters (Unicode code points) in a String. Typically created by String.iter.

String iterators pair a string with a valid byte index. This allows efficient character-by-character processing of strings while avoiding the need to manually ensure that byte indices are used with the correct strings.

An iterator is valid if the position i is valid for the string s, meaning 0 ≤ i ≤ s.endPos and i lies on a UTF8 byte boundary. If i = s.endPos, the iterator is at the end of the string.

Most operations on iterators return unspecified values if the iterator is not valid. The functions in the String.Iterator API rule out the creation of invalid iterators, with two exceptions:

• Iterator.next iter is invalid if iter is already at the end of the string (iter.atEnd is true), and
• Iterator.forward iter n/Iterator.nextn iter n is invalid if n is strictly greater than the number of remaining characters.

• s : String

  The string being iterated over.

• i : Pos

  The current UTF-8 byte position in the string s.

  This position is not guaranteed to be valid for the string. If the position is not valid, then the current character is (default : Char), similar to String.get on an invalid position.

instance String.instDecidableEqIterator : DecidableEq Iterator

Equations

• String.instDecidableEqIterator = String.decEqIterator✝

instance String.instInhabitedIterator : Inhabited Iterator

Equations

• String.instInhabitedIterator = { default := { s := default, i := default } }

@[inline]

def String.mkIterator (s : String) : Iterator

Creates an iterator at the beginning of the string.

Equations

• s.mkIterator = { s := s, i := 0 }

@[reducible, inline]

abbrev String.iter (s : String) : Iterator

Creates an iterator at the beginning of the string.

Equations

• String.iter = String.mkIterator

instance String.instSizeOfIterator : SizeOf Iterator

The size of a string iterator is the number of bytes remaining.

Recursive functions that iterate towards the end of a string will typically decrease this measure.

Equations

• String.instSizeOfIterator = { sizeOf := fun (i : String.Iterator) => i.s.utf8ByteSize - i.i.byteIdx }

theorem String.Iterator.sizeOf_eq (i : Iterator) : sizeOf i = i.s.utf8ByteSize - i.i.byteIdx

@[inline]

def String.Iterator.toString (self : Iterator) : String

The string being iterated over.

Equations

• String.Iterator.toString = String.Iterator.s

@[inline]

def String.Iterator.remainingBytes : Iterator → Nat

The number of UTF-8 bytes remaining in the iterator.

Equations

• { s := s, i := i }.remainingBytes = s.endPos.byteIdx - i.byteIdx

@[inline]

def String.Iterator.pos (self : Iterator) : Pos

The current UTF-8 byte position in the string s.

This position is not guaranteed to be valid for the string. If the position is not valid, then the current character is (default : Char), similar to String.get on an invalid position.

Equations

• String.Iterator.pos = String.Iterator.i

@[inline]

def String.Iterator.curr : Iterator → Char

Gets the character at the iterator's current position.

A run-time bounds check is performed. Use String.Iterator.curr' to avoid redundant bounds checks.

If the position is invalid, returns (default : Char).

Equations

• { s := s, i := i }.curr = s.get i

@[inline]

def String.Iterator.next : Iterator → Iterator

Moves the iterator's position forward by one character, unconditionally.

It is only valid to call this function if the iterator is not at the end of the string (i.e. if Iterator.atEnd is false); otherwise, the resulting iterator will be invalid.

Equations

• { s := s, i := i }.next = { s := s, i := s.next i }

@[inline]

def String.Iterator.prev : Iterator → Iterator

Moves the iterator's position backward by one character, unconditionally.

The position is not changed if the iterator is at the beginning of the string.

Equations

• { s := s, i := i }.prev = { s := s, i := s.prev i }

@[inline]

def String.Iterator.atEnd : Iterator → Bool

Checks whether the iterator is past its string's last character.

Equations

• { s := s, i := i }.atEnd = decide (i.byteIdx ≥ s.endPos.byteIdx)

@[inline]

def String.Iterator.hasNext : Iterator → Bool

Checks whether the iterator is at or before the string's last character.

Equations

• { s := s, i := i }.hasNext = decide (i.byteIdx < s.endPos.byteIdx)

@[inline]

def String.Iterator.hasPrev : Iterator → Bool

Checks whether the iterator is after the beginning of the string.

Equations

• { s := s, i := i }.hasPrev = decide (i.byteIdx > 0)

@[inline]

def String.Iterator.curr' (it : Iterator) (h : it.hasNext = true) : Char

Gets the character at the iterator's current position.

The proof of it.hasNext ensures that there is, in fact, a character at the current position. This function is faster that String.Iterator.curr due to avoiding a run-time bounds check.

Equations

• { s := s, i := i }.curr' h_2 = s.get' i ⋯

@[inline]

def String.Iterator.next' (it : Iterator) (h : it.hasNext = true) : Iterator

Moves the iterator's position forward by one character, unconditionally.

The proof of it.hasNext ensures that there is, in fact, a position that's one character forwards. This function is faster that String.Iterator.next due to avoiding a run-time bounds check.

Equations

• { s := s, i := i }.next' h_2 = { s := s, i := s.next' i ⋯ }

@[inline]

def String.Iterator.setCurr : Iterator → Char → Iterator

Replaces the current character in the string.

Does nothing if the iterator is at the end of the string. If both the replacement character and the replaced character are 7-bit ASCII characters and the string is not shared, then it is updated in-place and not copied.

Equations

• { s := s, i := i }.setCurr x✝ = { s := s.set i x✝, i := i }

@[inline]

def String.Iterator.toEnd : Iterator → Iterator

Moves the iterator's position to the end of the string, just past the last character.

Equations

• { s := s, i := i }.toEnd = { s := s, i := s.endPos }

@[inline]

def String.Iterator.extract : Iterator → Iterator → String

Extracts the substring between the positions of two iterators. The first iterator's position is the start of the substring, and the second iterator's position is the end.

Returns the empty string if the iterators are for different strings, or if the position of the first iterator is past the position of the second iterator.

Equations

• { s := a, i := a_1 }.extract { s := b, i := b_1 } = if (decide (a ≠ b) || decide (a_1 > b_1)) = true then "" else a.extract a_1 b_1

def String.Iterator.forward : Iterator → Nat → Iterator

Moves the iterator's position forward by the specified number of characters.

The resulting iterator is only valid if the number of characters to skip is less than or equal to the number of characters left in the iterator.

Equations

• x✝.forward 0 = x✝
• x✝.forward n.succ = x✝.next.forward n

@[inline]

def String.Iterator.remainingToString : Iterator → String

The remaining characters in an iterator, as a string.

Equations

• { s := s, i := i }.remainingToString = s.extract i s.endPos

def String.Iterator.nextn : Iterator → Nat → Iterator

Moves the iterator's position forward by the specified number of characters.

The resulting iterator is only valid if the number of characters to skip is less than or equal to the number of characters left in the iterator.

Equations

• x✝.nextn 0 = x✝
• x✝.nextn n.succ = x✝.next.nextn n

def String.Iterator.prevn : Iterator → Nat → Iterator

Moves the iterator's position back by the specified number of characters, stopping at the beginning of the string.

Equations

• x✝.prevn 0 = x✝
• x✝.prevn n.succ = x✝.prev.prevn n

@[irreducible]

def String.offsetOfPosAux (s : String) (pos i : Pos) (offset : Nat) : Nat

Equations

• s.offsetOfPosAux pos i offset = if i ≥ pos then offset else if h : s.atEnd i = true then offset else let_fun this := ⋯; s.offsetOfPosAux pos (s.next i) (offset + 1)

@[inline]

def String.offsetOfPos (s : String) (pos : Pos) : Nat

Returns the character index that corresponds to the provided position (i.e. UTF-8 byte index) in a string.

If the position is at the end of the string, then the string's length in characters is returned. If the position is invalid due to pointing at the middle of a UTF-8 byte sequence, then the character index of the next character after the position is returned.

Examples:

• "L∃∀N".offsetOfPos ⟨0⟩ = 0
• "L∃∀N".offsetOfPos ⟨1⟩ = 1
• "L∃∀N".offsetOfPos ⟨2⟩ = 2
• "L∃∀N".offsetOfPos ⟨4⟩ = 2
• "L∃∀N".offsetOfPos ⟨5⟩ = 3
• "L∃∀N".offsetOfPos ⟨50⟩ = 4

Equations

• s.offsetOfPos pos = s.offsetOfPosAux pos 0 0

@[irreducible, specialize #[]]

def String.foldlAux {α : Type u} (f : α → Char → α) (s : String) (stopPos i : Pos) (a : α) : α

Equations

• String.foldlAux f s stopPos i a = if h : i < stopPos then let_fun this := ⋯; String.foldlAux f s stopPos (s.next i) (f a (s.get i)) else a

@[inline]

def String.foldl {α : Type u} (f : α → Char → α) (init : α) (s : String) : α

Folds a function over a string from the left, accumulating a value starting with init. The accumulated value is combined with each character in order, using f.

Examples:

• "coffee tea water".foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 2
• "coffee tea and water".foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 3
• "coffee tea water".foldl (·.push ·) "" = "coffee tea water"

Equations

• String.foldl f init s = String.foldlAux f s s.endPos 0 init

@[irreducible, specialize #[]]

def String.foldrAux {α : Type u} (f : Char → α → α) (a : α) (s : String) (i begPos : Pos) : α

Equations

• String.foldrAux f a s i begPos = if h : begPos < i then let_fun this := ⋯; let i := s.prev i; let a := f (s.get i) a; String.foldrAux f a s i begPos else a

@[inline]

def String.foldr {α : Type u} (f : Char → α → α) (init : α) (s : String) : α

Folds a function over a string from the right, accumulating a value starting with init. The accumulated value is combined with each character in reverse order, using f.

Examples:

• "coffee tea water".foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 2
• "coffee tea and water".foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 3
• "coffee tea water".foldr (fun c s => c.push s) "" = "retaw dna aet eeffoc"

Equations

• String.foldr f init s = String.foldrAux f init s s.endPos 0

@[irreducible, specialize #[]]

def String.anyAux (s : String) (stopPos : Pos) (p : Char → Bool) (i : Pos) : Bool

Equations

• s.anyAux stopPos p i = if h : i < stopPos then if p (s.get i) = true then true else let_fun this := ⋯; s.anyAux stopPos p (s.next i) else false

@[inline]

def String.any (s : String) (p : Char → Bool) : Bool

Checks whether there is a character in a string for which the Boolean predicate p returns true.

Short-circuits at the first character for which p returns true.

Examples:

• "brown".any (·.isLetter) = true
• "brown".any (·.isWhitespace) = false
• "brown and orange".any (·.isLetter) = true
• "".any (fun _ => false) = false

Equations

• s.any p = s.anyAux s.endPos p 0

@[inline]

def String.all (s : String) (p : Char → Bool) : Bool

Checks whether the Boolean predicate p returns true for every character in a string.

Short-circuits at the first character for which p returns false.

Examples:

• "brown".all (·.isLetter) = true
• "brown and orange".all (·.isLetter) = false
• "".all (fun _ => false) = true

Equations

• s.all p = !s.any fun (c : Char) => !p c

@[inline]

def String.contains (s : String) (c : Char) : Bool

Checks whether a string contains the specified character.

Examples:

• "green".contains 'e' = true
• "green".contains 'x' = false
• "".contains 'x' = false

Equations

• s.contains c = s.any fun (a : Char) => a == c

theorem String.utf8SetAux_of_gt (c' : Char) (cs : List Char) {i p : Pos} : i > p → utf8SetAux c' cs i p = cs

theorem String.set_next_add (s : String) (i : Pos) (c : Char) (b₁ b₂ : Nat) (h : (s.next i).byteIdx + b₁ = s.endPos.byteIdx + b₂) : ((s.set i c).next i).byteIdx + b₁ = (s.set i c).endPos.byteIdx + b₂

theorem String.set_next_add.foo (i : Pos) (c : Char) (cs : List Char) (a : Pos) (b₁ b₂ : Nat) : (utf8GetAux cs a i).utf8Size + b₁ = utf8ByteSize.go cs + b₂ → (utf8GetAux (utf8SetAux c cs a i) a i).utf8Size + b₁ = utf8ByteSize.go (utf8SetAux c cs a i) + b₂

theorem String.mapAux_lemma (s : String) (i : Pos) (c : Char) (h : ¬s.atEnd i = true) : (s.set i c).endPos.byteIdx - ((s.set i c).next i).byteIdx < s.endPos.byteIdx - i.byteIdx

@[irreducible, specialize #[]]

def String.mapAux (f : Char → Char) (i : Pos) (s : String) : String

Equations

• String.mapAux f i s = if h : s.atEnd i = true then s else let c := f (s.get i); let_fun this := ⋯; let s := s.set i c; String.mapAux f (s.next i) s

@[inline]

def String.map (f : Char → Char) (s : String) : String

Applies the function f to every character in a string, returning a string that contains the resulting characters.

Examples:

• "abc123".map Char.toUpper = "ABC123"
• "".map Char.toUpper = ""

Equations

• String.map f s = String.mapAux f 0 s

@[inline]

def String.isNat (s : String) : Bool

Checks whether the string can be interpreted as the decimal representation of a natural number.

A string can be interpreted as a decimal natural number if it is not empty and all the characters in it are digits.

Use String.toNat? or String.toNat! to convert such a string to a natural number.

Examples:

• "".isNat = false
• "0".isNat = true
• "5".isNat = true
• "05".isNat = true
• "587".isNat = true
• "-587".isNat = false
• " 5".isNat = false
• "2+3".isNat = false
• "0xff".isNat = false

Equations

• s.isNat = (!s.isEmpty && s.all fun (x : Char) => x.isDigit)

def String.toNat? (s : String) : Option Nat

Interprets a string as the decimal representation of a natural number, returning it. Returns none if the string does not contain a decimal natural number.

A string can be interpreted as a decimal natural number if it is not empty and all the characters in it are digits.

Use String.isNat to check whether String.toNat? would return some. String.toNat! is an alternative that panics instead of returning none when the string is not a natural number.

Examples:

• "".toNat? = none
• "0".toNat? = some 0
• "5".toNat? = some 5
• "587".toNat? = some 587
• "-587".toNat? = none
• " 5".toNat? = none
• "2+3".toNat? = none
• "0xff".toNat? = none

Equations

• s.toNat? = if s.isNat = true then some (String.foldl (fun (n : Nat) (c : Char) => n * 10 + (c.toNat - '0'.toNat)) 0 s) else none

def String.substrEq (s1 : String) (pos1 : Pos) (s2 : String) (pos2 : Pos) (sz : Nat) : Bool

Checks whether substrings of two strings are equal. Substrings are indicated by their starting positions and a size in UTF-8 bytes. Returns false if the indicated substring does not exist in either string.

Equations

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

@[irreducible]

def String.substrEq.loop (s1 s2 : String) (off1 off2 stop1 : Pos) : Bool

Equations

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

def String.isPrefixOf (p s : String) : Bool

Checks whether the first string (p) is a prefix of the second (s).

String.startsWith is a version that takes the potential prefix after the string.

Examples:

• "red".isPrefixOf "red green blue" = true
• "green".isPrefixOf "red green blue" = false
• "".isPrefixOf "red green blue" = true

Equations

• p.isPrefixOf s = p.substrEq 0 s 0 p.endPos.byteIdx

def String.replace (s pattern replacement : String) : String

In the string s, replaces all occurrences of pattern with replacement.

Examples:

• "red green blue".replace "e" "" = "rd grn blu"
• "red green blue".replace "ee" "E" = "red grEn blue"
• "red green blue".replace "e" "E" = "rEd grEEn bluE"

Equations

• s.replace pattern replacement = if h : pattern.endPos.byteIdx = 0 then s else let_fun hPatt := ⋯; String.replace.loop s pattern replacement hPatt "" 0 0

@[irreducible]

def String.replace.loop (s pattern replacement : String) (hPatt : 0 < pattern.endPos.byteIdx) (acc : String) (accStop pos : Pos) : String

Equations

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

def String.findLineStart (s : String) (pos : Pos) : Pos

Returns the position of the beginning of the line that contains the position pos.

Lines are ended by '\n', and the returned position is either 0 : String.Pos or immediately after a '\n' character.

Equations

• s.findLineStart pos = match s.revFindAux (fun (x : Char) => decide (x = '\n')) pos with | none => 0 | some n => { byteIdx := n.byteIdx + 1 }

@[inline]

def Substring.isEmpty (ss : Substring) : Bool

Checks whether a substring is empty.

A substring is empty if its start and end positions are the same.

Equations

• ss.isEmpty = (ss.bsize == 0)

@[inline]

def Substring.toString : Substring → String

Copies the region of the underlying string pointed to by a substring into a fresh string.

Equations

• { str := s, startPos := b, stopPos := e }.toString = s.extract b e

@[inline]

def Substring.toIterator : Substring → String.Iterator

Returns an iterator into the underlying string, at the substring's starting position. The ending position is discarded, so the iterator alone cannot be used to determine whether its current position is within the original substring.

Equations

• { str := s, startPos := b, stopPos := e }.toIterator = { s := s, i := b }

@[inline]

def Substring.get : Substring → String.Pos → Char

Returns the character at the given position in the substring.

The position is relative to the substring, rather than the underlying string, and no bounds checking is performed with respect to the substring's end position. If the relative position is not a valid position in the underlying string, the fallback value (default : Char), which is 'A', is returned. Does not panic.

Equations

• { str := s, startPos := b, stopPos := stopPos }.get x✝ = s.get (b + x✝)

@[inline]

def Substring.next : Substring → String.Pos → String.Pos

Returns the next position in a substring after the given position. If the position is at the end of the substring, it is returned unmodified.

Both the input position and the returned position are interpreted relative to the substring's start position, not the underlying string.

Equations

• { str := s, startPos := b, stopPos := stopPos }.next x✝ = if b + x✝ = stopPos then x✝ else { byteIdx := (s.next (b + x✝)).byteIdx - b.byteIdx }

theorem Substring.lt_next (s : Substring) (i : String.Pos) (h : i.byteIdx < s.bsize) : i.byteIdx < (s.next i).byteIdx

@[inline]

def Substring.prev : Substring → String.Pos → String.Pos

Returns the previous position in a substring, just prior to the given position. If the position is at the beginning of the substring, it is returned unmodified.

Both the input position and the returned position are interpreted relative to the substring's start position, not the underlying string.

Equations

• { str := s, startPos := b, stopPos := stopPos }.prev x✝ = if b + x✝ = b then x✝ else { byteIdx := (s.prev (b + x✝)).byteIdx - b.byteIdx }

def Substring.nextn : Substring → Nat → String.Pos → String.Pos

Returns the position that's the specified number of characters forward from the given position in a substring. If the end position of the substring is reached, it is returned.

Both the input position and the returned position are interpreted relative to the substring's start position, not the underlying string.

Equations

• x✝¹.nextn 0 x✝ = x✝
• x✝¹.nextn i.succ x✝ = x✝¹.nextn i (x✝¹.next x✝)

def Substring.prevn : Substring → Nat → String.Pos → String.Pos

Returns the position that's the specified number of characters prior to the given position in a substring. If the start position of the substring is reached, it is returned.

Both the input position and the returned position are interpreted relative to the substring's start position, not the underlying string.

Equations

• x✝¹.prevn 0 x✝ = x✝
• x✝¹.prevn i.succ x✝ = x✝¹.prevn i (x✝¹.prev x✝)

@[inline]

def Substring.front (s : Substring) : Char

Returns the first character in the substring.

If the substring is empty, but the substring's start position is a valid position in the underlying string, then the character at the start position is returned. If the substring's start position is not a valid position in the string, the fallback value (default : Char), which is 'A', is returned. Does not panic.

Equations

• s.front = s.get 0

@[inline]

def Substring.posOf (s : Substring) (c : Char) : String.Pos

Returns the substring-relative position of the first occurrence of c in s, or s.bsize if c doesn't occur.

Equations

• { str := s_1, startPos := b, stopPos := e }.posOf c = { byteIdx := (s_1.posOfAux c e b).byteIdx - b.byteIdx }

@[inline]

def Substring.drop : Substring → Nat → Substring

Removes the specified number of characters (Unicode code points) from the beginning of a substring by advancing its start position.

If the substring's end position is reached, the start position is not advanced past it.

Equations

• { str := s, startPos := b, stopPos := e }.drop x✝ = { str := s, startPos := b + { str := s, startPos := b, stopPos := e }.nextn x✝ 0, stopPos := e }

@[inline]

def Substring.dropRight : Substring → Nat → Substring

Removes the specified number of characters (Unicode code points) from the end of a substring by moving its end position towards its start position.

If the substring's start position is reached, the end position is not retracted past it.

Equations

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

@[inline]

def Substring.take : Substring → Nat → Substring

Retains only the specified number of characters (Unicode code points) at the beginning of a substring, by moving its end position towards its start position.

If the substring's start position is reached, the end position is not retracted past it.

Equations

• { str := s, startPos := b, stopPos := e }.take x✝ = { str := s, startPos := b, stopPos := b + { str := s, startPos := b, stopPos := e }.nextn x✝ 0 }

@[inline]

def Substring.takeRight : Substring → Nat → Substring

Retains only the specified number of characters (Unicode code points) at the end of a substring, by moving its start position towards its end position.

If the substring's end position is reached, the start position is not advanced past it.

Equations

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

@[inline]

def Substring.atEnd : Substring → String.Pos → Bool

Checks whether a position in a substring is precisely equal to its ending position.

The position is understood relative to the substring's starting position, rather than the underlying string's starting position.

Equations

• { str := s, startPos := b, stopPos := stopPos }.atEnd x✝ = (b + x✝ == stopPos)

@[inline]

def Substring.extract : Substring → String.Pos → String.Pos → Substring

Returns the region of the substring delimited by the provided start and stop positions, as a substring. The positions are interpreted with respect to the substring's start position, rather than the underlying string.

If the resulting substring is empty, then the resulting substring is a substring of the empty string "". Otherwise, the underlying string is that of the input substring with the beginning and end positions adjusted.

Equations

• { str := s, startPos := b, stopPos := e }.extract x✝¹ x✝ = if x✝¹ ≥ x✝ then { str := "", startPos := 0, stopPos := 0 } else { str := s, startPos := e.min (b + x✝¹), stopPos := e.min (b + x✝) }

def Substring.splitOn (s : Substring) (sep : String := " ") : List Substring

Splits a substring s on occurrences of the separator string sep. The default separator is " ".

When sep is empty, the result is [s]. When sep occurs in overlapping patterns, the first match is taken. There will always be exactly n+1 elements in the returned list if there were n non-overlapping matches of sep in the string. The separators are not included in the returned substrings, which are all substrings of s's string.

Equations

• s.splitOn sep = if (sep == "") = true then [s] else Substring.splitOn.loop s sep 0 0 0 []

@[irreducible]

def Substring.splitOn.loop (s : Substring) (sep : String := " ") (b i j : String.Pos) (r : List Substring) : List Substring

Equations

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

@[inline]

def Substring.foldl {α : Type u} (f : α → Char → α) (init : α) (s : Substring) : α

Folds a function over a substring from the left, accumulating a value starting with init. The accumulated value is combined with each character in order, using f.

Equations

• Substring.foldl f init { str := s_1, startPos := b, stopPos := e } = String.foldlAux f s_1 e b init

@[inline]

def Substring.foldr {α : Type u} (f : Char → α → α) (init : α) (s : Substring) : α

Folds a function over a substring from the right, accumulating a value starting with init. The accumulated value is combined with each character in reverse order, using f.

Equations

• Substring.foldr f init { str := s_1, startPos := b, stopPos := e } = String.foldrAux f init s_1 e b

@[inline]

def Substring.any (s : Substring) (p : Char → Bool) : Bool

Checks whether the Boolean predicate p returns true for any character in a substring.

Short-circuits at the first character for which p returns true.

Equations

• { str := s_1, startPos := b, stopPos := e }.any p = s_1.anyAux e p b

@[inline]

def Substring.all (s : Substring) (p : Char → Bool) : Bool

Checks whether the Boolean predicate p returns true for every character in a substring.

Short-circuits at the first character for which p returns false.

Equations

• s.all p = !s.any fun (c : Char) => !p c

@[inline]

def Substring.contains (s : Substring) (c : Char) : Bool

Checks whether a substring contains the specified character.

Equations

• s.contains c = s.any fun (a : Char) => a == c

@[irreducible, specialize #[]]

def Substring.takeWhileAux (s : String) (stopPos : String.Pos) (p : Char → Bool) (i : String.Pos) : String.Pos

Equations

• Substring.takeWhileAux s stopPos p i = if h : i < stopPos then if p (s.get i) = true then let_fun this := ⋯; Substring.takeWhileAux s stopPos p (s.next i) else i else i

@[inline]

def Substring.takeWhile : Substring → (Char → Bool) → Substring

Retains only the longest prefix of a substring in which a Boolean predicate returns true for all characters by moving the substring's end position towards its start position.

Equations

• { str := s, startPos := b, stopPos := e }.takeWhile x✝ = { str := s, startPos := b, stopPos := Substring.takeWhileAux s e x✝ b }

@[inline]

def Substring.dropWhile : Substring → (Char → Bool) → Substring

Removes the longest prefix of a substring in which a Boolean predicate returns true for all characters by moving the substring's start position. The start position is moved to the position of the first character for which the predicate returns false, or to the substring's end position if the predicate always returns true.

Equations

• { str := s, startPos := b, stopPos := e }.dropWhile x✝ = { str := s, startPos := Substring.takeWhileAux s e x✝ b, stopPos := e }

@[irreducible, specialize #[]]

def Substring.takeRightWhileAux (s : String) (begPos : String.Pos) (p : Char → Bool) (i : String.Pos) : String.Pos

Equations

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

@[inline]

def Substring.takeRightWhile : Substring → (Char → Bool) → Substring

Retains only the longest suffix of a substring in which a Boolean predicate returns true for all characters by moving the substring's start position towards its end position.

Equations

• { str := s, startPos := b, stopPos := e }.takeRightWhile x✝ = { str := s, startPos := Substring.takeRightWhileAux s b x✝ e, stopPos := e }

@[inline]

def Substring.dropRightWhile : Substring → (Char → Bool) → Substring

Removes the longest suffix of a substring in which a Boolean predicate returns true for all characters by moving the substring's end position. The end position is moved just after the position of the last character for which the predicate returns false, or to the substring's start position if the predicate always returns true.

Equations

• { str := s, startPos := b, stopPos := e }.dropRightWhile x✝ = { str := s, startPos := b, stopPos := Substring.takeRightWhileAux s b x✝ e }

@[inline]

def Substring.trimLeft (s : Substring) : Substring

Removes leading whitespace from a substring by moving its start position to the first non-whitespace character, or to its end position if there is no non-whitespace character.

“Whitespace” is defined as characters for which Char.isWhitespace returns true.

Equations

• s.trimLeft = s.dropWhile Char.isWhitespace

@[inline]

def Substring.trimRight (s : Substring) : Substring

Removes trailing whitespace from a substring by moving its end position to the last non-whitespace character, or to its start position if there is no non-whitespace character.

“Whitespace” is defined as characters for which Char.isWhitespace returns true.

Equations

• s.trimRight = s.dropRightWhile Char.isWhitespace

@[inline]

def Substring.trim : Substring → Substring

Removes leading and trailing whitespace from a substring by first moving its start position to the first non-whitespace character, and then moving its end position to the last non-whitespace character.

If the substring consists only of whitespace, then the resulting substring's start position is moved to its end position.

“Whitespace” is defined as characters for which Char.isWhitespace returns true.

Examples:

• " red green blue ".toSubstring.trim.toString = "red green blue"
• " red green blue ".toSubstring.trim.startPos = ⟨1⟩
• " red green blue ".toSubstring.trim.stopPos = ⟨15⟩
• " ".toSubstring.trim.startPos = ⟨5⟩

Equations

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

@[inline]

def Substring.isNat (s : Substring) : Bool

Checks whether the substring can be interpreted as the decimal representation of a natural number.

A substring can be interpreted as a decimal natural number if it is not empty and all the characters in it are digits.

Use Substring.toNat? to convert such a substring to a natural number.

Equations

• s.isNat = s.all fun (c : Char) => c.isDigit

def Substring.toNat? (s : Substring) : Option Nat

Checks whether the substring can be interpreted as the decimal representation of a natural number, returning the number if it can.

A substring can be interpreted as a decimal natural number if it is not empty and all the characters in it are digits.

Use Substring.isNat to check whether the substring is such a substring.

Equations

• s.toNat? = if s.isNat = true then some (Substring.foldl (fun (n : Nat) (c : Char) => n * 10 + (c.toNat - '0'.toNat)) 0 s) else none

def Substring.beq (ss1 ss2 : Substring) : Bool

Checks whether two substrings represent equal strings. Usually accessed via the == operator.

Two substrings do not need to have the same underlying string or the same start and end positions; instead, they are equal if they contain the same sequence of characters.

Equations

• ss1.beq ss2 = (ss1.bsize == ss2.bsize && ss1.str.substrEq ss1.startPos ss2.str ss2.startPos ss1.bsize)

instance Substring.hasBeq : BEq Substring

Equations

• Substring.hasBeq = { beq := Substring.beq }

def Substring.sameAs (ss1 ss2 : Substring) : Bool

Checks whether two substrings have the same position and content.

The two substrings do not need to have the same underlying string for this check to succeed.

Equations

• ss1.sameAs ss2 = (ss1.startPos == ss2.startPos && ss1 == ss2)

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

Returns the longest common prefix of two substrings.

The returned substring uses 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 t : Substring) (spos 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 t : Substring) : Substring

Returns the longest common suffix of two substrings.

The returned substring uses 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 t : Substring) (spos 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 pre : Substring) : Option Substring

If pre is a prefix of s, returns the remainder. Returns none otherwise.

The substring pre is a prefix of s if there exists a t : Substring such that s.toString = pre.toString ++ t.toString. If so, the result is the substring of s without the prefix.

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 suff : Substring) : Option Substring

If suff is a suffix of s, returns the remainder. Returns none otherwise.

The substring suff is a suffix of s if there exists a t : Substring such that s.toString = t.toString ++ suff.toString. If so, the result the substring of s without the suffix.

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

@[inline]

def String.drop (s : String) (n : Nat) : String

Removes the specified number of characters (Unicode code points) from the start of the string.

If n is greater than s.length, returns "".

Examples:

• "red green blue".drop 4 = "green blue"
• "red green blue".drop 10 = "blue"
• "red green blue".drop 50 = ""

Equations

• s.drop n = (s.toSubstring.drop n).toString

@[inline]

def String.dropRight (s : String) (n : Nat) : String

Removes the specified number of characters (Unicode code points) from the end of the string.

If n is greater than s.length, returns "".

Examples:

• "red green blue".dropRight 5 = "red green"
• "red green blue".dropRight 11 = "red"
• "red green blue".dropRight 50 = ""

Equations

• s.dropRight n = (s.toSubstring.dropRight n).toString

@[inline]

def String.take (s : String) (n : Nat) : String

Creates a new string that contains the first n characters (Unicode code points) of s.

If n is greater than s.length, returns s.

Examples:

• "red green blue".take 3 = "red"
• "red green blue".take 1 = "r"
• "red green blue".take 0 = ""
• "red green blue".take 100 = "red green blue"

Equations

• s.take n = (s.toSubstring.take n).toString

@[inline]

def String.takeRight (s : String) (n : Nat) : String

Creates a new string that contains the last n characters (Unicode code points) of s.

If n is greater than s.length, returns s.

Examples:

• "red green blue".takeRight 4 = "blue"
• "red green blue".takeRight 1 = "e"
• "red green blue".takeRight 0 = ""
• "red green blue".takeRight 100 = "red green blue"

Equations

• s.takeRight n = (s.toSubstring.takeRight n).toString

@[inline]

def String.takeWhile (s : String) (p : Char → Bool) : String

Creates a new string that contains the longest prefix of s in which p returns true for all characters.

Examples:

• "red green blue".takeWhile (·.isLetter) = "red"
• "red green blue".takeWhile (· == 'r') = "r"
• "red green blue".takeWhile (· != 'n') = "red gree"
• "red green blue".takeWhile (fun _ => true) = "red green blue"

Equations

• s.takeWhile p = (s.toSubstring.takeWhile p).toString

@[inline]

def String.dropWhile (s : String) (p : Char → Bool) : String

Creates a new string by removing the longest prefix from s in which p returns true for all characters.

Examples:

• "red green blue".dropWhile (·.isLetter) = " green blue"
• "red green blue".dropWhile (· == 'r') = "ed green blue"
• "red green blue".dropWhile (· != 'n') = "n blue"
• "red green blue".dropWhile (fun _ => true) = ""

Equations

• s.dropWhile p = (s.toSubstring.dropWhile p).toString

@[inline]

def String.takeRightWhile (s : String) (p : Char → Bool) : String

Creates a new string that contains the longest suffix of s in which p returns true for all characters.

Examples:

• "red green blue".takeRightWhile (·.isLetter) = "blue"
• "red green blue".takeRightWhile (· == 'e') = "e"
• "red green blue".takeRightWhile (· != 'n') = " blue"
• "red green blue".takeRightWhile (fun _ => true) = "red green blue"

Equations

• s.takeRightWhile p = (s.toSubstring.takeRightWhile p).toString

@[inline]

def String.dropRightWhile (s : String) (p : Char → Bool) : String

Creates a new string by removing the longest suffix from s in which p returns true for all characters.

Examples:

• "red green blue".dropRightWhile (·.isLetter) = "red green "
• "red green blue".dropRightWhile (· == 'e') = "red green blu"
• "red green blue".dropRightWhile (· != 'n') = "red green"
• "red green blue".dropRightWhile (fun _ => true) = ""

Equations

• s.dropRightWhile p = (s.toSubstring.dropRightWhile p).toString

@[inline]

def String.startsWith (s pre : String) : Bool

Checks whether the first string (s) begins with the second (pre).

String.isPrefix is a version that takes the potential prefix before the string.

Examples:

• "red green blue".startsWith "red" = true
• "red green blue".startsWith "green" = false
• "red green blue".startsWith "" = true
• "red".startsWith "red" = true

Equations

• s.startsWith pre = (s.toSubstring.take pre.length == pre.toSubstring)

@[inline]

def String.endsWith (s post : String) : Bool

Checks whether the first string (s) ends with the second (post).

Examples:

• "red green blue".endsWith "blue" = true
• "red green blue".endsWith "green" = false
• "red green blue".endsWith "" = true
• "red".endsWith "red" = true

Equations

• s.endsWith post = (s.toSubstring.takeRight post.length == post.toSubstring)

@[inline]

def String.trimRight (s : String) : String

Removes trailing whitespace from a string.

“Whitespace” is defined as characters for which Char.isWhitespace returns true.

Examples:

• "abc".trimRight = "abc"
• " abc".trimRight = " abc"
• "abc \t ".trimRight = "abc"
• " abc ".trimRight = " abc"
• "abc\ndef\n".trimRight = "abc\ndef"

Equations

• s.trimRight = s.toSubstring.trimRight.toString

@[inline]

def String.trimLeft (s : String) : String

Removes leading whitespace from a string.

“Whitespace” is defined as characters for which Char.isWhitespace returns true.

Examples:

• "abc".trimLeft = "abc"
• " abc".trimLeft = " abc"
• "abc \t ".trimLeft = "abc \t "
• " abc ".trimLeft = "abc "
• "abc\ndef\n".trimLeft = "abc\ndef\n"

Equations

• s.trimLeft = s.toSubstring.trimLeft.toString

@[inline]

def String.trim (s : String) : String

Removes leading and trailing whitespace from a string.

“Whitespace” is defined as characters for which Char.isWhitespace returns true.

Examples:

• "abc".trim = "abc"
• " abc".trim = "abc"
• "abc \t ".trim = "abc"
• " abc ".trim = "abc"
• "abc\ndef\n".trim = "abc\ndef"

Equations

• s.trim = s.toSubstring.trim.toString

@[inline]

def String.nextWhile (s : String) (p : Char → Bool) (i : Pos) : Pos

Repeatedly increments a position in a string, as if by String.next, while the predicate p returns true for the character at the position. Stops incrementing at the end of the string or when p returns false for the current character.

Examples:

• let s := " a "; s.get (s.nextWhile Char.isWhitespace 0) = 'a'
• let s := "a "; s.get (s.nextWhile Char.isWhitespace 0) = 'a'
• let s := "ba "; s.get (s.nextWhile Char.isWhitespace 0) = 'b'

Equations

• s.nextWhile p i = Substring.takeWhileAux s s.endPos p i

@[inline]

def String.nextUntil (s : String) (p : Char → Bool) (i : Pos) : Pos

Repeatedly increments a position in a string, as if by String.next, while the predicate p returns false for the character at the position. Stops incrementing at the end of the string or when p returns true for the current character.

Examples:

• let s := " a "; s.get (s.nextUntil Char.isWhitespace 0) = ' '
• let s := " a "; s.get (s.nextUntil Char.isLetter 0) = 'a'
• let s := "a "; s.get (s.nextUntil Char.isWhitespace 0) = ' '

Equations

• s.nextUntil p i = s.nextWhile (fun (c : Char) => !p c) i

@[inline]

def String.toUpper (s : String) : String

Replaces each character in s with the result of applying Char.toUpper to it.

Char.toUpper has no effect on characters outside of the range 'a'–'z'.

Examples:

• "orange".toUpper = "ORANGE"
• "abc123".toUpper = "ABC123"

Equations

• s.toUpper = String.map Char.toUpper s

@[inline]

def String.toLower (s : String) : String

Replaces each character in s with the result of applying Char.toLower to it.

Char.toLower has no effect on characters outside of the range 'A'–'Z'.

Examples:

• "ORANGE".toLower = "orange"
• "Orange".toLower = "orange"
• "ABc123".toLower = "abc123"

Equations

• s.toLower = String.map Char.toLower s

@[inline]

def String.capitalize (s : String) : String

Replaces the first character in s with the result of applying Char.toUpper to it. Returns the empty string if the string is empty.

Char.toUpper has no effect on characters outside of the range 'a'–'z'.

Examples:

• "orange".capitalize = "Orange"
• "ORANGE".capitalize = "ORANGE"
• "".capitalize = ""

Equations

• s.capitalize = s.set 0 (s.get 0).toUpper

@[inline]

def String.decapitalize (s : String) : String

Replaces the first character in s with the result of applying Char.toLower to it. Returns the empty string if the string is empty.

Char.toLower has no effect on characters outside of the range 'A'–'Z'.

Examples:

• "Orange".decapitalize = "orange"
• "ORANGE".decapitalize = "oRANGE"
• "".decapitalize = ""

Equations

• s.decapitalize = s.set 0 (s.get 0).toLower

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

If pre is a prefix of s, returns the remainder. Returns none otherwise.

The string pre is a prefix of s if there exists a t : String such that s = pre ++ t. If so, the result is some t.

Use String.stripPrefix to return the string unchanged when pre is not a prefix.

Examples:

• "red green blue".dropPrefix? "red " = some "green blue"
• "red green blue".dropPrefix? "reed " = none
• "red green blue".dropPrefix? "" = some "red green blue"

Equations

• s.dropPrefix? pre = s.toSubstring.dropPrefix? pre.toSubstring

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

If suff is a suffix of s, returns the remainder. Returns none otherwise.

The string suff is a suffix of s if there exists a t : String such that s = t ++ suff. If so, the result is some t.

Use String.stripSuffix to return the string unchanged when suff is not a suffix.

Examples:

• "red green blue".dropSuffix? " blue" = some "red green"
• "red green blue".dropSuffix? " blu " = none
• "red green blue".dropSuffix? "" = some "red green blue"

Equations

• s.dropSuffix? suff = s.toSubstring.dropSuffix? suff.toSubstring

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

If pre is a prefix of s, returns the remainder. Returns s unmodified otherwise.

The string pre is a prefix of s if there exists a t : String such that s = pre ++ t. If so, the result is t. Otherwise, it is s.

Use String.dropPrefix? to return none when pre is not a prefix.

Examples:

• "red green blue".stripPrefix "red " = "green blue"
• "red green blue".stripPrefix "reed " = "red green blue"
• "red green blue".stripPrefix "" = "red green blue"

Equations

• s.stripPrefix pre = (Option.map Substring.toString (s.dropPrefix? pre)).getD s

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

If suff is a suffix of s, returns the remainder. Returns s unmodified otherwise.

The string suff is a suffix of s if there exists a t : String such that s = t ++ suff. If so, the result is t. Otherwise, it is s.

Use String.dropSuffix? to return none when suff is not a suffix.

Examples:

• "red green blue".stripSuffix " blue" = "red green"
• "red green blue".stripSuffix " blu " = "red green blue"
• "red green blue".stripSuffix "" = "red green blue"

Equations

• s.stripSuffix suff = (Option.map Substring.toString (s.dropSuffix? suff)).getD s

@[inline]

def Char.toString (c : Char) : String

Constructs a singleton string that contains only the provided character.

Examples:

• 'L'.toString = "L"
• '"'.toString = "\""

Equations

• c.toString = String.singleton c

@[simp]

theorem Char.length_toString (c : Char) : c.toString.length = 1

theorem String.ext {s₁ s₂ : String} (h : s₁.data = s₂.data) : s₁ = s₂

theorem String.ext_iff {s₁ s₂ : String} : s₁ = s₂ ↔ s₁.data = s₂.data

@[simp]

theorem String.default_eq : default = ""

@[simp]

theorem String.length_mk (s : List Char) : { data := s }.length = s.length

@[simp]

theorem String.length_empty : "".length = 0

@[simp]

theorem String.length_singleton (c : Char) : (singleton c).length = 1

@[simp]

theorem String.length_push {s : String} (c : Char) : (s.push c).length = s.length + 1

@[simp]

theorem String.length_pushn {s : String} (c : Char) (n : Nat) : (s.pushn c n).length = s.length + n

@[simp]

theorem String.length_append (s t : String) : (s ++ t).length = s.length + t.length

@[simp]

theorem String.data_push (s : String) (c : Char) : (s.push c).data = s.data ++ [c]

@[simp]

theorem String.data_append (s t : String) : (s ++ t).data = s.data ++ t.data

theorem String.lt_iff {s t : String} : s < t ↔ s.data < t.data

@[simp]

theorem String.Pos.byteIdx_zero : byteIdx 0 = 0

theorem String.Pos.byteIdx_mk (n : Nat) : { byteIdx := n }.byteIdx = n

@[simp]

theorem String.Pos.mk_zero : { } = 0

@[simp]

theorem String.Pos.mk_byteIdx (p : Pos) : { byteIdx := p.byteIdx } = p

theorem String.Pos.ext {i₁ i₂ : Pos} (h : i₁.byteIdx = i₂.byteIdx) : i₁ = i₂

theorem String.Pos.ext_iff {i₁ i₂ : Pos} : i₁ = i₂ ↔ i₁.byteIdx = i₂.byteIdx

@[simp]

theorem String.Pos.add_byteIdx (p₁ p₂ : Pos) : (p₁ + p₂).byteIdx = p₁.byteIdx + p₂.byteIdx

theorem String.Pos.add_eq (p₁ p₂ : Pos) : p₁ + p₂ = { byteIdx := p₁.byteIdx + p₂.byteIdx }

@[simp]

theorem String.Pos.sub_byteIdx (p₁ p₂ : Pos) : (p₁ - p₂).byteIdx = p₁.byteIdx - p₂.byteIdx

theorem String.Pos.sub_eq (p₁ p₂ : Pos) : p₁ - p₂ = { byteIdx := p₁.byteIdx - p₂.byteIdx }

@[simp]

theorem String.Pos.addChar_byteIdx (p : Pos) (c : Char) : (p + c).byteIdx = p.byteIdx + c.utf8Size

theorem String.Pos.addChar_eq (p : Pos) (c : Char) : p + c = { byteIdx := p.byteIdx + c.utf8Size }

theorem String.Pos.zero_addChar_byteIdx (c : Char) : (0 + c).byteIdx = c.utf8Size

theorem String.Pos.zero_addChar_eq (c : Char) : 0 + c = { byteIdx := c.utf8Size }

theorem String.Pos.addChar_right_comm (p : Pos) (c₁ c₂ : Char) : p + c₁ + c₂ = p + c₂ + c₁

theorem String.Pos.ne_of_lt {i₁ i₂ : Pos} (h : i₁ < i₂) : i₁ ≠ i₂

theorem String.Pos.ne_of_gt {i₁ i₂ : Pos} (h : i₁ < i₂) : i₂ ≠ i₁

@[simp]

theorem String.Pos.byteIdx_addString (p : Pos) (s : String) : (p + s).byteIdx = p.byteIdx + s.utf8ByteSize

@[reducible, inline, deprecated String.Pos.byteIdx_addString (since := "2025-03-18")]

abbrev String.Pos.addString_byteIdx (p : Pos) (s : String) : (p + s).byteIdx = p.byteIdx + s.utf8ByteSize

Equations

• String.Pos.addString_byteIdx = String.Pos.byteIdx_addString

theorem String.Pos.addString_eq (p : Pos) (s : String) : p + s = { byteIdx := p.byteIdx + s.utf8ByteSize }

theorem String.Pos.byteIdx_zero_addString (s : String) : (0 + s).byteIdx = s.utf8ByteSize

@[reducible, inline, deprecated String.Pos.byteIdx_zero_addString (since := "2025-03-18")]

abbrev String.Pos.zero_addString_byteIdx (s : String) : (0 + s).byteIdx = s.utf8ByteSize

Equations

• String.Pos.zero_addString_byteIdx = String.Pos.byteIdx_zero_addString

theorem String.Pos.zero_addString_eq (s : String) : 0 + s = { byteIdx := s.utf8ByteSize }

theorem String.Pos.le_iff {i₁ i₂ : Pos} : i₁ ≤ i₂ ↔ i₁.byteIdx ≤ i₂.byteIdx

@[simp]

theorem String.Pos.mk_le_mk {i₁ i₂ : Nat} : { byteIdx := i₁ } ≤ { byteIdx := i₂ } ↔ i₁ ≤ i₂

theorem String.Pos.lt_iff {i₁ i₂ : Pos} : i₁ < i₂ ↔ i₁.byteIdx < i₂.byteIdx

@[simp]

theorem String.Pos.mk_lt_mk {i₁ i₂ : Nat} : { byteIdx := i₁ } < { byteIdx := i₂ } ↔ i₁ < i₂

@[simp]

theorem String.get!_eq_get (s : String) (p : Pos) : s.get! p = s.get p

theorem String.lt_next' (s : String) (p : Pos) : p < s.next p

@[simp]

theorem String.prev_zero (s : String) : s.prev 0 = 0

@[simp]

theorem String.get'_eq (s : String) (p : Pos) (h : ¬s.atEnd p = true) : s.get' p h = s.get p

@[simp]

theorem String.next'_eq (s : String) (p : Pos) (h : ¬s.atEnd p = true) : s.next' p h = s.next p

theorem String.singleton_eq (c : Char) : singleton c = { data := [c] }

@[simp]

theorem String.data_singleton (c : Char) : (singleton c).data = [c]

@[simp]

theorem String.append_empty (s : String) : s ++ "" = s

@[simp]

theorem String.empty_append (s : String) : "" ++ s = s

theorem String.append_assoc (s₁ s₂ s₃ : String) : s₁ ++ s₂ ++ s₃ = s₁ ++ (s₂ ++ s₃)

@[simp]

theorem Substring.prev_zero (s : Substring) : s.prev 0 = 0

@[simp]

theorem Substring.prevn_zero (s : Substring) (n : Nat) : s.prevn n 0 = 0