Documentation

Init.Data.String.Basic

Equations
Equations
Equations
@[extern lean_string_dec_lt]
instance String.decidableLT (s₁ s₂ : String) :
Decidable (s₁ < s₂)
Equations
@[reducible, inline, deprecated String.decidableLT (since := "2024-12-13")]
abbrev String.decLt (s₁ s₂ : String) :
Decidable (s₁ < s₂)
Equations
@[reducible]
def String.le (a b : String) :
Equations
instance String.decLE (s₁ s₂ : String) :
Decidable (s₁ s₂)
Equations
@[extern lean_string_length]

Returns the length of a string in Unicode code points.

Examples:

Equations
@[extern lean_string_push]

Pushes a character onto the end of a string.

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

Example: "abc".push 'd' = "abcd"

Equations
  • { data := s }.push x✝ = { data := s ++ [x✝] }
@[extern lean_string_append]

Appends two strings.

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

Example: "abc".append "def" = "abcdef"

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

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, because the compiler uses an optimized representation as dynamic arrays.

Example: "abc".toList = ['a', 'b', 'c']

Equations
@[extern lean_string_is_valid_pos]

Returns true if p is a valid UTF-8 position in the string s, meaning that p ≤ s.endPos and p lies on a UTF-8 character boundary. This has an O(1) implementation in the runtime.

Equations
Equations
Equations
@[extern lean_string_utf8_get]
def String.get (s : String) (p : Pos) :

Returns the character at position p of a string. If p is not a valid position, returns (default : Char).

See utf8GetAux for the reference implementation.

Examples:

  • "abc".get ⟨1⟩ = 'b'
  • "abc".get ⟨3⟩ = (default : Char) = 'A'

Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8 character. For example,"L∃∀N".get ⟨2⟩ = (default : Char) = 'A'.

Equations
Equations
@[extern lean_string_utf8_get_opt]

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

Examples:

  • "abc".get? ⟨1⟩ = some 'b'
  • "abc".get? ⟨3⟩ = none

Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8 character. For example, "L∃∀N".get? ⟨2⟩ = none

Equations
@[extern lean_string_utf8_get_bang]
def String.get! (s : String) (p : Pos) :

Returns the character at position p of a string. If p is not a valid position, returns (default : Char) and produces a panic error message.

Examples:

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

Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8 character. For example, "L∃∀N".get! ⟨2⟩ panics.

Equations
def String.utf8SetAux (c' : Char) :
List CharPosPosList Char
Equations
@[extern lean_string_utf8_set]
def String.set :
StringPosCharString

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 ASCII characters and the string is not shared, destructive updates are used.

Examples:

  • "abc".set ⟨1⟩ 'B' = "aBc"
  • "abc".set ⟨3⟩ 'D' = "abc"
  • "L∃∀N".set ⟨4⟩ 'X' = "L∃XN"

Because '∃' is a multi-byte character, the byte index 2 in L∃∀N is an invalid position, so "L∃∀N".set ⟨2⟩ 'X' = "L∃∀N".

Equations
def String.modify (s : String) (i : Pos) (f : CharChar) :

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.

Examples:

Equations
@[extern lean_string_utf8_next]
def String.next (s : String) (p : Pos) :

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

Examples: Given def abc := "abc" and def lean := "L∃∀N",

  • abc.get (0 |> abc.next) = 'b'
  • lean.get (0 |> lean.next |> lean.next) = '∀'

Cases where the result is unspecified:

  • "abc".next ⟨3⟩, since 3 = s.endPos
  • "L∃∀N".next ⟨2⟩, since 2 points into the middle of a multi-byte UTF-8 character
Equations
Equations
@[extern lean_string_utf8_prev]
def String.prev :
StringPosPos

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.

Examples: Given def abc := "abc" and def lean := "L∃∀N",

  • abc.get (abc.endPos |> abc.prev) = 'c'
  • lean.get (lean.endPos |> lean.prev |> lean.prev |> lean.prev) = '∃'
  • "L∃∀N".prev ⟨3⟩ is unspecified, since byte 3 occurs in the middle of the multi-byte character '∃'.
Equations
@[inline]

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

Examples:

Equations
@[inline]

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

Examples:

  • "abc".back = 'c'
  • "".back = (default : Char)
Equations
@[extern lean_string_utf8_at_end]

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

Examples: Given def abc := "abc" and def lean := "L∃∀N",

Because "L∃∀N" contains multi-byte characters, lean.next (lean.next 0) is not equal to abc.next (abc.next 0).

Equations
@[extern lean_string_utf8_get_fast]
def String.get' (s : String) (p : Pos) (h : ¬s.atEnd p = true) :

Returns the character at position p of a string. If p is not a valid position, returns (default : Char).

Requires evidence, h, that p is within bounds instead of performing a runtime bounds check as in get.

Examples:

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

A typical pattern combines get' with a dependent if-else 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).

Equations
@[extern lean_string_utf8_next_fast]
def String.next' (s : String) (p : Pos) (h : ¬s.atEnd p = true) :

Returns the next position in a string after position p. If p is not a valid position, the result is unspecified.

Requires evidence, h, that p is within bounds instead of performing a runtime bounds check as in next.

Examples:

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

A typical pattern combines next' with a dependent if-else 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)
Equations
@[reducible, inline, deprecated Char.utf8Size_pos (since := "2026-06-04")]
Equations
@[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) :
theorem String.Pos.ne_zero_of_lt {a b : Pos} :
a < bb 0
theorem String.lt_next (s : String) (i : Pos) :
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) :
@[irreducible]
def String.posOfAux (s : String) (c : Char) (stopPos pos : Pos) :
Equations
@[inline]
def String.posOf (s : String) (c : Char) :

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

Examples:

  • "abba".posOf 'a' = ⟨0⟩
  • "abba".posOf 'z' = ⟨4⟩
  • "L∃∀N".posOf '∀' = ⟨4⟩
Equations
@[irreducible]
def String.revPosOfAux (s : String) (c : Char) (pos : Pos) :
Equations
@[inline]

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

Examples:

  • "abba".posOf 'a' = some ⟨3⟩
  • "abba".posOf 'z' = none
  • "L∃∀N".posOf '∀' = some ⟨4⟩
Equations
@[irreducible]
def String.findAux (s : String) (p : CharBool) (stopPos pos : Pos) :
Equations
@[inline]
def String.find (s : String) (p : CharBool) :
Equations
@[irreducible]
def String.revFindAux (s : String) (p : CharBool) (pos : Pos) :
Equations
@[inline]
def String.revFind (s : String) (p : CharBool) :
Equations
@[reducible, inline]
abbrev String.Pos.min (p₁ p₂ : Pos) :
Equations

Returns the first position where the two strings differ.

Equations
@[irreducible]
def String.firstDiffPos.loop (a b : String) (stopPos i : Pos) :
Equations
  • One or more equations did not get rendered due to their size.
@[extern lean_string_utf8_extract]
Equations
Equations
Equations
@[irreducible, specialize #[]]
def String.splitAux (s : String) (p : CharBool) (b i : Pos) (r : List String) :
Equations
  • One or more equations did not get rendered due to their size.
@[specialize #[]]
def String.split (s : String) (p : CharBool) :
Equations
@[irreducible]
def String.splitOnAux (s sep : String) (b i j : Pos) (r : 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 := " ") :

Splits a string s on occurrences of the separator sep. When sep is empty, it returns [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 nonoverlapping matches of sep in the string. The default separator is " ". The separators are not included in the returned substrings.

"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
@[inline]
def String.pushn (s : String) (c : Char) (n : Nat) :
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations

Iterator over the characters (Char) of a String.

Typically created by s.iter, where s is a String.

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 arbitrary values if the iterator is not valid. The functions in the String.Iterator API should rule out the creation of invalid iterators, with two exceptions:

  • s : String

    The string the iterator is for.

  • i : Pos

    The current position.

    This position is not necessarily valid for the string, for instance if one keeps calling Iterator.next when Iterator.atEnd is true. If the position is not valid, then the current character is (default : Char), similar to String.get on an invalid position.

Instances For
@[inline]

Creates an iterator at the beginning of a string.

Equations
@[reducible, inline]

Creates an iterator at the beginning of a string.

Equations

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

Equations
@[inline]

The string the iterator is for.

Equations
@[inline]

Number of bytes remaining in the iterator.

Equations
@[inline]

The current position.

This position is not necessarily valid for the string, for instance if one keeps calling Iterator.next when Iterator.atEnd is true. If the position is not valid, then the current character is (default : Char), similar to String.get on an invalid position.

Equations
@[inline]

The character at the current position.

On an invalid position, returns (default : Char).

Equations
@[inline]

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. Iterator.atEnd is false; otherwise, the resulting iterator will be invalid.

Equations
  • { s := s, i := i }.next = { s := s, i := s.next i }
@[inline]

Decreases the iterator's position.

If the position is zero, this function is the identity.

Equations
  • { s := s, i := i }.prev = { s := s, i := s.prev i }
@[inline]

True if the iterator is past the string's last character.

Equations
@[inline]

True if the iterator is not past the string's last character.

Equations
@[inline]

True if the position is not zero.

Equations
@[inline]
Equations
@[inline]
Equations
  • { s := s, i := i }.next' h_2 = { s := s, i := s.next' i }
@[inline]

Replaces the current character in the string.

Does nothing if the iterator is at the end of the string. If the iterator contains the only reference to its string, this function will mutate the string in-place instead of allocating a new one.

Equations
  • { s := s, i := i }.setCurr x✝ = { s := s.set i x✝, i := i }
@[inline]

Moves the iterator's position to the end of the string.

Note that i.toEnd.atEnd is always true.

Equations
@[inline]

Extracts the substring between the positions of two iterators.

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

Moves the iterator's position several characters forward.

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
@[inline]

The remaining characters in an iterator, as a string.

Equations

Moves the iterator's position several characters forward.

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

Moves the iterator's position several characters back.

If asked to go back more characters than available, stops at the beginning of the string.

Equations
@[irreducible]
def String.offsetOfPosAux (s : String) (pos i : Pos) (offset : Nat) :
Equations
@[inline]
def String.offsetOfPos (s : String) (pos : Pos) :
Equations
@[irreducible, specialize #[]]
def String.foldlAux {α : Type u} (f : αCharα) (s : String) (stopPos i : Pos) (a : α) :
α
Equations
@[inline]
def String.foldl {α : Type u} (f : αCharα) (init : α) (s : String) :
α
Equations
@[irreducible, specialize #[]]
def String.foldrAux {α : Type u} (f : Charαα) (a : α) (s : String) (i begPos : Pos) :
α
Equations
@[inline]
def String.foldr {α : Type u} (f : Charαα) (init : α) (s : String) :
α
Equations
@[irreducible, specialize #[]]
def String.anyAux (s : String) (stopPos : Pos) (p : CharBool) (i : Pos) :
Equations
@[inline]
def String.any (s : String) (p : CharBool) :
Equations
@[inline]
def String.all (s : String) (p : CharBool) :
Equations
@[inline]
def String.contains (s : String) (c : Char) :
Equations
theorem String.utf8SetAux_of_gt (c' : Char) (cs : List Char) {i p : Pos} :
i > putf8SetAux 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) :
@[irreducible, specialize #[]]
def String.mapAux (f : CharChar) (i : Pos) (s : String) :
Equations
@[inline]
def String.map (f : CharChar) (s : String) :
Equations
@[inline]
Equations
Equations
def String.substrEq (s1 : String) (off1 : Pos) (s2 : String) (off2 : Pos) (sz : Nat) :

Return true iff the substring of byte size sz starting at position off1 in s1 is equal to that starting at off2 in s2.. False if either substring of that byte size does not exist.

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) :
Equations
  • One or more equations did not get rendered due to their size.

Return true iff p is a prefix of s

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

Replace all occurrences of pattern in s with replacement.

Equations
@[irreducible]
def String.replace.loop (s pattern replacement : String) (hPatt : 0 < pattern.endPos.byteIdx) (acc : String) (accStop pos : Pos) :
Equations
  • One or more equations did not get rendered due to their size.
def String.findLineStart (s : String) (pos : Pos) :

Return the beginning of the line that contains character pos.

Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
  • { str := s, startPos := b, stopPos := e }.toIterator = { s := s, i := b }
@[inline]

Return the codepoint at the given offset into the substring.

Equations
  • { str := s, startPos := b, stopPos := stopPos }.get x✝ = s.get (b + x✝)
@[inline]

Given an offset of a codepoint into the substring, return the offset there of the next codepoint.

Equations
@[inline]

Given an offset of a codepoint into the substring, return the offset there of the previous codepoint.

Equations
Equations
Equations
@[inline]
Equations
@[inline]

Return the offset into s of the first occurrence of c in s, or s.bsize if c doesn't occur.

Equations
@[inline]
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]
Equations
  • One or more equations did not get rendered due to their size.
@[inline]
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]
Equations
  • One or more equations did not get rendered due to their size.
@[inline]
Equations
  • { str := s, startPos := b, stopPos := stopPos }.atEnd x✝ = (b + x✝ == stopPos)
@[inline]
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 := " ") :
Equations
@[irreducible]
def Substring.splitOn.loop (s : Substring) (sep : String := " ") (b i j : String.Pos) (r : 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) :
α
Equations
@[inline]
def Substring.foldr {α : Type u} (f : Charαα) (init : α) (s : Substring) :
α
Equations
@[inline]
def Substring.any (s : Substring) (p : CharBool) :
Equations
  • { str := s_1, startPos := b, stopPos := e }.any p = s_1.anyAux e p b
@[inline]
def Substring.all (s : Substring) (p : CharBool) :
Equations
@[inline]
Equations
@[irreducible, specialize #[]]
def Substring.takeWhileAux (s : String) (stopPos : String.Pos) (p : CharBool) (i : String.Pos) :
Equations
@[inline]
Equations
@[inline]
Equations
@[irreducible, specialize #[]]
Equations
  • One or more equations did not get rendered due to their size.
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
  • One or more equations did not get rendered due to their size.
@[inline]
Equations
Equations
def Substring.beq (ss1 ss2 : Substring) :
Equations

Checks whether two substrings have the same position and content.

Equations

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

Equations
@[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.

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

Equations
@[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.

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

Equations

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

Equations
@[inline]
def String.drop (s : String) (n : Nat) :
Equations
@[inline]
Equations
@[inline]
def String.take (s : String) (n : Nat) :
Equations
@[inline]
Equations
@[inline]
def String.takeWhile (s : String) (p : CharBool) :
Equations
@[inline]
def String.dropWhile (s : String) (p : CharBool) :
Equations
@[inline]
Equations
@[inline]
def String.endsWith (s post : String) :
Equations
@[inline]
Equations
@[inline]
def String.nextWhile (s : String) (p : CharBool) (i : Pos) :
Equations
@[inline]
def String.nextUntil (s : String) (p : CharBool) (i : Pos) :
Equations
@[inline]
Equations
@[inline]
Equations

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

Equations

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

Equations

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

Equations

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

Equations
@[inline]
Equations
@[simp]
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]
@[simp]
theorem String.length_mk (s : List Char) :
{ data := s }.length = s.length
@[simp]
@[simp]
@[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
theorem String.Pos.byteIdx_mk (n : Nat) :
{ byteIdx := n }.byteIdx = n
@[simp]
theorem String.Pos.mk_zero :
{ byteIdx := 0 } = 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) :
theorem String.Pos.addChar_eq (p : Pos) (c : Char) :
p + c = { byteIdx := p.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₁
theorem String.Pos.addString_eq (p : Pos) (s : String) :
p + s = { byteIdx := p.byteIdx + s.utf8ByteSize }
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]
@[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