Strings

This file builds on the UTF-8 verification in Init.Data.String.Decode and the preliminary material in Init.Data.String.Defs to get the theory of strings off the ground. In particular, in this file we construct the decoding function String.data : String → List Char and show that it is a two-sided inverse to List.asString : List Char → String. This in turn enables us to understand the validity predicate on positions in terms of lists of characters, which forms the basis for all further verification for strings.

@[simp]

theorem String.utf8ByteSize_singleton {c : Char} : (singleton c).utf8ByteSize = c.utf8Size

theorem List.isUTF8FirstByte_getElem_utf8Encode_singleton {c : Char} {i : Nat} {hi : i < [c].utf8Encode.size} : [c].utf8Encode[i].IsUTF8FirstByte ↔ i = 0

theorem ByteArray.IsValidUTF8.push {b : ByteArray} (h : b.IsValidUTF8) {c : Char} (hc : c.utf8Size = 1) : (b.push c.toUInt8).IsValidUTF8

theorem ByteArray.isValidUTF8_utf8Encode_singleton_append_iff {b : ByteArray} {c : Char} : ([c].utf8Encode ++ b).IsValidUTF8 ↔ b.IsValidUTF8

@[inline]

def ByteArray.utf8Decode? (b : ByteArray) : Option (Array Char)

Decodes a sequence of characters from their UTF-8 representation. Returns none if the bytes are not a sequence of Unicode scalar values.

def ByteArray.utf8Decode?.go (b : ByteArray) (i : Nat) (acc : Array Char) (hi : i ≤ b.size) : Option (Array Char)

@[extern lean_string_validate_utf8]

def ByteArray.validateUTF8 (b : ByteArray) : Bool

def ByteArray.validateUTF8.go (b : ByteArray) (i : Nat) (hi : i ≤ b.size) : Bool

theorem ByteArray.isSome_utf8Decode?Go_eq_validateUTF8Go {b : ByteArray} {i : Nat} {acc : Array Char} {hi : i ≤ b.size} : (utf8Decode?.go b i acc hi).isSome = validateUTF8.go b i hi

theorem ByteArray.isSome_utf8Decode?_eq_validateUTF8 {b : ByteArray} : b.utf8Decode?.isSome = b.validateUTF8

@[simp]

theorem ByteArray.utf8Decode?_empty : empty.utf8Decode? = some #[]

theorem ByteArray.isSome_utf8Decode?_iff {b : ByteArray} : b.utf8Decode?.isSome = true ↔ b.IsValidUTF8

@[simp]

theorem ByteArray.validateUTF8_eq_true_iff {b : ByteArray} : b.validateUTF8 = true ↔ b.IsValidUTF8

@[simp]

theorem ByteArray.validateUTF8_eq_false_iff {b : ByteArray} : b.validateUTF8 = false ↔ ¬b.IsValidUTF8

instance instDecidableIsValidUTF8 {b : ByteArray} : Decidable b.IsValidUTF8

@[inline]

def String.fromUTF8? (a : ByteArray) : Option String

Decodes an array of bytes that encode a string as UTF-8 into the corresponding string, or returns none if the array is not a valid UTF-8 encoding of a string.

@[inline]

def String.fromUTF8! (a : ByteArray) : String

Decodes an array of bytes that encode a string as UTF-8 into the corresponding string, or panics if the array is not a valid UTF-8 encoding of a string.

@[simp]

theorem String.empty_append {s : String} : "" ++ s = s

@[simp]

theorem String.append_empty {s : String} : s ++ "" = s

@[simp]

theorem String.ofList_nil : ofList [] = ""

@[deprecated String.ofList_nil (since := "2025-10-30")]

theorem List.asString_nil : String.ofList [] = ""

@[simp]

theorem String.ofList_append {l₁ l₂ : List Char} : ofList (l₁ ++ l₂) = ofList l₁ ++ ofList l₂

@[deprecated String.ofList_append (since := "2025-10-30")]

theorem List.asString_append {l₁ l₂ : List Char} : String.ofList (l₁ ++ l₂) = String.ofList l₁ ++ String.ofList l₂

def String.Internal.toArray (b : String) : Array Char

@[simp]

theorem String.Internal.toArray_empty : toArray "" = #[]

@[extern lean_string_data]

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

Converts a string to a list of characters.

Since strings are represented as dynamic arrays of bytes containing the string encoded using UTF-8, this operation takes time and space linear in the length of the string.

Examples:

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

@[extern lean_string_data, deprecated String.toList (since := "2025-10-30")]

def String.data (b : String) : List Char

Converts a string to a list of characters.

Since strings are represented as dynamic arrays of bytes containing the string encoded using UTF-8, this operation takes time and space linear in the length of the string.

Examples:

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

@[simp]

theorem String.toList_empty : "".toList = []

@[deprecated String.toList_empty (since := "2025-10-30")]

theorem String.data_empty : "".toList = []

@[extern lean_string_length]

def String.length (b : String) : Nat

Returns the length of a string in Unicode code points.

Examples:

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

@[simp]

theorem String.Internal.size_toArray {b : String} : (toArray b).size = b.length

@[simp]

theorem String.length_toList {s : String} : s.toList.length = s.length

@[deprecated String.length_toList (since := "2025-10-30")]

theorem String.length_data {b : String} : b.toList.length = b.length

theorem ByteArray.utf8Decode?_utf8Encode_singleton_append {l : ByteArray} {c : Char} : ([c].utf8Encode ++ l).utf8Decode? = Option.map (fun (x : Array Char) => #[c] ++ x) l.utf8Decode?

@[simp]

theorem List.utf8Decode?_utf8Encode {l : List Char} : l.utf8Encode.utf8Decode? = some l.toArray

@[simp]

theorem ByteArray.utf8Encode_get_utf8Decode? {b : ByteArray} {h : b.utf8Decode?.isSome = true} : (b.utf8Decode?.get h).toList.utf8Encode = b

@[simp]

theorem String.toList_ofList {l : List Char} : (ofList l).toList = l

@[deprecated String.toList_ofList (since := "2025-10-30")]

theorem List.data_asString {l : List Char} : (String.ofList l).toList = l

@[simp]

theorem String.ofList_toList {s : String} : ofList s.toList = s

@[deprecated String.ofList_toList (since := "2025-10-30")]

theorem String.asString_data {b : String} : ofList b.toList = b

theorem String.ofList_injective {l₁ l₂ : List Char} (h : ofList l₁ = ofList l₂) : l₁ = l₂

@[deprecated String.ofList_injective (since := "2025-10-30")]

theorem List.asString_injective {l₁ l₂ : List Char} (h : String.ofList l₁ = String.ofList l₂) : l₁ = l₂

theorem String.ofList_inj {l₁ l₂ : List Char} : ofList l₁ = ofList l₂ ↔ l₁ = l₂

@[deprecated String.ofList_inj (since := "2025-10-30")]

theorem List.asString_inj {l₁ l₂ : List Char} : String.ofList l₁ = String.ofList l₂ ↔ l₁ = l₂

theorem String.toList_injective {s₁ s₂ : String} (h : s₁.toList = s₂.toList) : s₁ = s₂

@[deprecated String.toList_injective (since := "2025-10-30")]

theorem String.data_injective {s₁ s₂ : String} (h : s₁.toList = s₂.toList) : s₁ = s₂

theorem String.toList_inj {s₁ s₂ : String} : s₁.toList = s₂.toList ↔ s₁ = s₂

@[deprecated String.toList_inj (since := "2025-10-30")]

theorem String.data_inj {s₁ s₂ : String} : s₁.toList = s₂.toList ↔ s₁ = s₂

@[simp]

theorem String.toList_append {s t : String} : (s ++ t).toList = s.toList ++ t.toList

@[deprecated String.toList_append (since := "2025-10-30")]

theorem String.data_append {l₁ l₂ : String} : (l₁ ++ l₂).toList = l₁.toList ++ l₂.toList

@[simp]

theorem String.utf8Encode_toList {b : String} : b.toList.utf8Encode = b.toByteArray

@[deprecated String.utf8Encode_toList (since := "2025-10-30")]

theorem String.utf8encode_data {b : String} : b.toList.utf8Encode = b.toByteArray

@[simp]

theorem String.toList_eq_nil_iff {b : String} : b.toList = [] ↔ b = ""

@[deprecated String.toList_eq_nil_iff (since := "2025-10-30")]

theorem String.data_eq_nil_iff {b : String} : b.toList = [] ↔ b = ""

@[simp]

theorem String.ofList_eq_empty_iff {l : List Char} : ofList l = "" ↔ l = []

@[deprecated String.ofList_eq_empty_iff (since := "2025-10-30")]

theorem List.asString_eq_empty_iff {l : List Char} : String.ofList l = "" ↔ l = []

@[simp]

theorem String.length_ofList {l : List Char} : (ofList l).length = l.length

@[deprecated String.length_ofList (since := "2025-10-30")]

theorem List.length_asString {l : List Char} : (String.ofList l).length = l.length

instance String.instLT : LT String

@[extern lean_string_dec_lt]

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

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

instance String.instLE : LE String

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

theorem List.isPrefix_of_utf8Encode_append_eq_utf8Encode {l m : List Char} (b : ByteArray) (h : l.utf8Encode ++ b = m.utf8Encode) : l <+: m

theorem String.Pos.Raw.IsValid.exists {s : String} {p : Raw} (h : IsValid s p) : ∃ (m₁ : List Char), ∃ (m₂ : List Char), m₁.utf8Encode = s.toByteArray.extract 0 p.byteIdx ∧ ofList (m₁ ++ m₂) = s

theorem String.Pos.Raw.IsValid.isValidUTF8_extract_utf8ByteSize {s : String} {p : Raw} (h : IsValid s p) : (s.toByteArray.extract p.byteIdx s.utf8ByteSize).IsValidUTF8

theorem String.Pos.Raw.isValid_iff_exists_append {s : String} {p : Raw} : IsValid s p ↔ ∃ (s₁ : String), ∃ (s₂ : String), s = s₁ ++ s₂ ∧ p = s₁.rawEndPos

theorem String.Pos.Raw.isValid_ofList {l : List Char} {p : Raw} : IsValid (ofList l) p ↔ ∃ (i : Nat), p.byteIdx = (ofList (List.take i l)).utf8ByteSize

@[deprecated String.Pos.Raw.isValid_ofList (since := "2025-10-30")]

theorem String.Pos.Raw.isValid_asString {l : List Char} {p : Raw} : IsValid (ofList l) p ↔ ∃ (i : Nat), p.byteIdx = (ofList (List.take i l)).utf8ByteSize

theorem String.Pos.Raw.isValid_iff_exists_take_toList {s : String} {p : Raw} : IsValid s p ↔ ∃ (i : Nat), p.byteIdx = (ofList (List.take i s.toList)).utf8ByteSize

@[deprecated String.Pos.Raw.isValid_iff_exists_take_toList (since := "2025-10-30")]

theorem String.Pos.Raw.isValid_iff_exists_take_data {s : String} {p : Raw} : IsValid s p ↔ ∃ (i : Nat), p.byteIdx = (ofList (List.take i s.toList)).utf8ByteSize

@[simp]

theorem String.Pos.Raw.isValid_singleton {c : Char} {p : Raw} : IsValid (singleton c) p ↔ p = 0 ∨ p.byteIdx = c.utf8Size

theorem String.Pos.Raw.isValid_append {s t : String} {p : Raw} : IsValid (s ++ t) p ↔ IsValid s p ∨ s.rawEndPos ≤ p ∧ IsValid t (p - s)

theorem String.Pos.Raw.IsValid.append_left {t : String} {p : Raw} (h : IsValid t p) (s : String) : IsValid (s ++ t) (s + p)

theorem String.Pos.Raw.IsValid.append_right {s : String} {p : Raw} (h : IsValid s p) (t : String) : IsValid (s ++ t) p

theorem String.Pos.Raw.isValid_push {s : String} {c : Char} {p : Raw} : IsValid (s.push c) p ↔ IsValid s p ∨ p = s.rawEndPos + c

@[simp]

theorem String.utf8ByteSize_push {s : String} {c : Char} : (s.push c).utf8ByteSize = s.utf8ByteSize + c.utf8Size

@[simp]

theorem String.rawEndPos_push {s : String} {c : Char} : (s.push c).rawEndPos = s.rawEndPos + c

@[deprecated String.rawEndPos_push (since := "2025-10-20")]

theorem String.endPos_push {s : String} {c : Char} : (s.push c).rawEndPos = s.rawEndPos + c

theorem String.push_induction (s : String) (motive : String → Prop) (empty : motive "") (push : ∀ (b : String) (c : Char), motive b → motive (b.push c)) : motive s

theorem String.Pos.Raw.isValid_iff_isUTF8FirstByte {s : String} {p : Raw} : IsValid s p ↔ p = s.rawEndPos ∨ ∃ (h : p < s.rawEndPos), (s.getUTF8Byte p h).IsUTF8FirstByte

@[extern lean_string_is_valid_pos]

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

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

This means that p ≤ s.rawEndPos 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

@[simp]

theorem String.Pos.Raw.isValid_eq_true_iff {s : String} {p : Raw} : isValid s p = true ↔ IsValid s p

@[simp]

theorem String.Pos.Raw.isValid_eq_false_iff {s : String} {p : Raw} : isValid s p = false ↔ ¬IsValid s p

instance String.instDecidableIsValid {s : String} {p : Pos.Raw} : Decidable (Pos.Raw.IsValid s p)

theorem String.Pos.Raw.isValid_iff_isSome_utf8DecodeChar? {s : String} {p : Raw} : IsValid s p ↔ p = s.rawEndPos ∨ (s.toByteArray.utf8DecodeChar? p.byteIdx).isSome = true

theorem ByteArray.IsValidUTF8.isUTF8FirstByte_getElem_zero {b : ByteArray} (h : b.IsValidUTF8) (h₀ : 0 < b.size) : b[0].IsUTF8FirstByte

theorem String.isUTF8FirstByte_getUTF8Byte_zero {b : String} {h : 0 < b.rawEndPos} : (b.getUTF8Byte 0 h).IsUTF8FirstByte

theorem String.Pos.Raw.isValidUTF8_extract_iff {s : String} (p₁ p₂ : Raw) (hle : p₁ ≤ p₂) (hle' : p₂ ≤ s.rawEndPos) : (s.toByteArray.extract p₁.byteIdx p₂.byteIdx).IsValidUTF8 ↔ p₁ = p₂ ∨ IsValid s p₁ ∧ IsValid s p₂

theorem String.Pos.Raw.isValid_iff_isValidUTF8_extract_utf8ByteSize {s : String} {p : Raw} : IsValid s p ↔ p ≤ s.rawEndPos ∧ (s.toByteArray.extract p.byteIdx s.utf8ByteSize).IsValidUTF8

theorem String.Pos.isValidUTF8_extract {s : String} (pos₁ pos₂ : s.Pos) : (s.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx).IsValidUTF8

@[extern lean_string_utf8_extract]

def String.extract {s : String} (b e : s.Pos) : String

Copies a region of a string to a new string.

The region of s from b (inclusive) to e (exclusive) is copied to a newly-allocated String.

If b's offset is greater than or equal to that of e, then the resulting string is "".

If possible, prefer String.slice, which avoids the allocation.

@[deprecated String.extract (since := "2025-12-01")]

def String.Pos.extract {s : String} (b e : s.Pos) : String

@[simp]

theorem String.toByteArray_extract {s : String} {b e : s.Pos} : (extract b e).toByteArray = s.toByteArray.extract b.offset.byteIdx e.offset.byteIdx

@[inline]

def String.Slice.copy (s : Slice) : String

Creates a String from a String.Slice by copying the bytes.

theorem String.Slice.toByteArray_copy {s : Slice} : s.copy.toByteArray = s.str.toByteArray.extract s.startInclusive.offset.byteIdx s.endExclusive.offset.byteIdx

@[simp]

theorem String.Slice.utf8ByteSize_copy {s : Slice} : s.copy.utf8ByteSize = s.endExclusive.offset.byteIdx - s.startInclusive.offset.byteIdx

@[simp]

theorem String.Slice.rawEndPos_copy {s : Slice} : s.copy.rawEndPos = s.rawEndPos

@[simp]

theorem String.copy_toSlice {s : String} : s.toSlice.copy = s

theorem String.Slice.getUTF8Byte_eq_getUTF8Byte_copy {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} : s.getUTF8Byte p h = s.copy.getUTF8Byte p ⋯

theorem String.Slice.getUTF8Byte_copy {s : Slice} {p : Pos.Raw} {h : p < s.copy.rawEndPos} : s.copy.getUTF8Byte p h = s.getUTF8Byte p ⋯

theorem String.Slice.isUTF8FirstByte_utf8ByteAt_zero {s : Slice} {h : 0 < s.rawEndPos} : (s.getUTF8Byte 0 h).IsUTF8FirstByte

@[simp]

theorem String.Pos.Raw.isValid_copy_iff {s : Slice} {p : Raw} : IsValid s.copy p ↔ IsValidForSlice s p

theorem String.Pos.Raw.isValidForSlice_iff_isUTF8FirstByte {s : Slice} {p : Raw} : IsValidForSlice s p ↔ p = s.rawEndPos ∨ ∃ (h : p < s.rawEndPos), (s.getUTF8Byte p h).IsUTF8FirstByte

def String.Pos.Raw.isValidForSlice (s : Slice) (p : Raw) : Bool

Efficiently checks whether a position is at a UTF-8 character boundary of the slice s.

@[simp]

theorem String.Pos.Raw.isValidForSlice_eq_true_iff {s : Slice} {p : Raw} : isValidForSlice s p = true ↔ IsValidForSlice s p

@[simp]

theorem String.Pos.Raw.isValidForSlice_eq_false_iff {s : Slice} {p : Raw} : isValidForSlice s p = false ↔ ¬IsValidForSlice s p

instance String.instDecidableIsValidForSlice {s : Slice} {p : Pos.Raw} : Decidable (Pos.Raw.IsValidForSlice s p)

theorem String.Pos.Raw.isValidForSlice_iff_isSome_utf8DecodeChar?_copy {s : Slice} {p : Raw} : IsValidForSlice s p ↔ p = s.rawEndPos ∨ (s.copy.toByteArray.utf8DecodeChar? p.byteIdx).isSome = true

theorem String.Slice.toByteArray_str_eq {s : Slice} : s.str.toByteArray = s.str.toByteArray.extract 0 s.startInclusive.offset.byteIdx ++ s.copy.toByteArray ++ s.str.toByteArray.extract s.endExclusive.offset.byteIdx s.str.toByteArray.size

theorem String.Pos.Raw.isValidForSlice_iff_isSome_utf8DecodeChar? {s : Slice} {p : Raw} : IsValidForSlice s p ↔ p = s.rawEndPos ∨ p < s.rawEndPos ∧ (s.str.toByteArray.utf8DecodeChar? (s.startInclusive.offset.byteIdx + p.byteIdx)).isSome = true

theorem String.Slice.Pos.isUTF8FirstByte_byte {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos} : (pos.byte h).IsUTF8FirstByte

@[inline]

def String.Slice.Pos.str {s : Slice} (pos : s.Pos) : s.str.Pos

Given a valid position on a slice s, obtains the corresponding valid position on the underlying string s.str.

@[simp]

theorem String.Slice.Pos.offset_str {s : Slice} {pos : s.Pos} : pos.str.offset = pos.offset.offsetBy s.startInclusive.offset

@[simp]

theorem String.Slice.Pos.offset_str_le_offset_endExclusive {s : Slice} {pos : s.Pos} : pos.str.offset ≤ s.endExclusive.offset

theorem String.Slice.Pos.offset_le_offset_str {s : Slice} {pos : s.Pos} : pos.offset ≤ pos.str.offset

@[simp]

theorem String.Slice.Pos.offset_le_offset_endExclusive {s : Slice} {pos : s.Pos} : pos.offset ≤ s.endExclusive.offset

@[simp]

theorem String.Slice.Pos.startInclusive_le_str {s : Slice} {pos : s.Pos} : s.startInclusive ≤ pos.str

@[inline]

def String.Slice.Pos.ofStr {s : Slice} (pos : s.str.Pos) (h₁ : s.startInclusive ≤ pos) (h₂ : pos ≤ s.endExclusive) : s.Pos

Given a valid position on s.str which is within the bounds of the slice s, obtains the corresponding valid position on s.

@[simp]

theorem String.Slice.Pos.offset_ofStr {s : Slice} {pos : s.str.Pos} {h₁ : s.startInclusive ≤ pos} {h₂ : pos ≤ s.endExclusive} : (ofStr pos h₁ h₂).offset = pos.offset.unoffsetBy s.startInclusive.offset

@[inline]

def String.Slice.sliceFrom (s : Slice) (pos : s.Pos) : Slice

Given a slice and a valid position within the slice, obtain a new slice on the same underlying string by replacing the start of the slice with the given position.

@[deprecated String.Slice.sliceFrom (since := "2025-11-20")]

def String.Slice.replaceStart (s : Slice) (pos : s.Pos) : Slice

@[simp]

theorem String.Slice.str_sliceFrom {s : Slice} {pos : s.Pos} : (s.sliceFrom pos).str = s.str

@[simp]

theorem String.Slice.startInclusive_sliceFrom {s : Slice} {pos : s.Pos} : (s.sliceFrom pos).startInclusive = pos.str

@[simp]

theorem String.Slice.endExclusive_sliceFrom {s : Slice} {pos : s.Pos} : (s.sliceFrom pos).endExclusive = s.endExclusive

@[inline]

def String.Slice.sliceTo (s : Slice) (pos : s.Pos) : Slice

Given a slice and a valid position within the slice, obtain a new slice on the same underlying string by replacing the end of the slice with the given position.

@[deprecated String.Slice.sliceTo (since := "2025-11-20")]

def String.Slice.replaceEnd (s : Slice) (pos : s.Pos) : Slice

@[simp]

theorem String.Slice.str_sliceTo {s : Slice} {pos : s.Pos} : (s.sliceTo pos).str = s.str

@[simp]

theorem String.Slice.startInclusive_sliceTo {s : Slice} {pos : s.Pos} : (s.sliceTo pos).startInclusive = s.startInclusive

@[simp]

theorem String.Slice.endExclusive_sliceTo {s : Slice} {pos : s.Pos} : (s.sliceTo pos).endExclusive = pos.str

@[inline]

def String.Slice.slice (s : Slice) (newStart newEnd : s.Pos) (h : newStart ≤ newEnd) : Slice

Given a slice and two valid positions within the slice, obtain a new slice on the same underlying string formed by the new bounds.

@[deprecated String.Slice.slice (since := "2025-11-20")]

def String.Slice.replaceStartEnd (s : Slice) (newStart newEnd : s.Pos) (h : newStart ≤ newEnd) : Slice

@[simp]

theorem String.Slice.str_slice {s : Slice} {newStart newEnd : s.Pos} {h : newStart ≤ newEnd} : (s.slice newStart newEnd h).str = s.str

@[simp]

theorem String.Slice.startInclusive_slice {s : Slice} {newStart newEnd : s.Pos} {h : newStart ≤ newEnd} : (s.slice newStart newEnd h).startInclusive = newStart.str

@[simp]

theorem String.Slice.endExclusive_slice {s : Slice} {newStart newEnd : s.Pos} {h : newStart ≤ newEnd} : (s.slice newStart newEnd h).endExclusive = newEnd.str

def String.Slice.slice? (s : Slice) (newStart newEnd : s.Pos) : Option Slice

Given a slice and two valid positions within the slice, obtain a new slice on the same underlying string formed by the new bounds, or none if the given end is strictly less than the given start.

def String.Slice.slice! (s : Slice) (newStart newEnd : s.Pos) : Slice

Given a slice and two valid positions within the slice, obtain a new slice on the same underlying string formed by the new bounds, or panic if the given end is strictly less than the given start.

@[deprecated String.Slice.slice! (since := "2025-11-20")]

def String.Slice.replaceStartEnd! (s : Slice) (newStart newEnd : s.Pos) : Slice

@[simp]

theorem String.Slice.utf8ByteSize_sliceFrom {s : Slice} {pos : s.Pos} : (s.sliceFrom pos).utf8ByteSize = s.utf8ByteSize - pos.offset.byteIdx

theorem String.Slice.rawEndPos_sliceFrom {s : Slice} {pos : s.Pos} : (s.sliceFrom pos).rawEndPos = s.rawEndPos.unoffsetBy pos.offset

@[simp]

theorem String.Slice.utf8ByteSize_sliceTo {s : Slice} {pos : s.Pos} : (s.sliceTo pos).utf8ByteSize = pos.offset.byteIdx

@[simp]

theorem String.Slice.rawEndPos_sliceTo {s : Slice} {pos : s.Pos} : (s.sliceTo pos).rawEndPos = pos.offset

@[simp]

theorem String.Slice.utf8ByteSize_slice {s : Slice} {newStart newEnd : s.Pos} {h : newStart ≤ newEnd} : (s.slice newStart newEnd h).utf8ByteSize = newStart.offset.byteDistance newEnd.offset

theorem String.Pos.Raw.isValidForSlice_sliceFrom {s : Slice} {p : s.Pos} {off : Raw} : IsValidForSlice (s.sliceFrom p) off ↔ IsValidForSlice s (off.offsetBy p.offset)

theorem String.Pos.Raw.isValidForSlice_sliceTo {s : Slice} {p : s.Pos} {off : Raw} : IsValidForSlice (s.sliceTo p) off ↔ off ≤ p.offset ∧ IsValidForSlice s off

@[extern lean_string_utf8_get_fast]

def String.decodeChar (s : String) (byteIdx : Nat) (h : (s.toByteArray.utf8DecodeChar? byteIdx).isSome = true) : Char

@[inline]

def String.Slice.Pos.get {s : Slice} (pos : s.Pos) (h : pos ≠ s.endPos) : Char

Obtains the character at the given position in the string.

theorem String.Slice.Pos.get_eq_utf8DecodeChar {s : Slice} (pos : s.Pos) (h : pos ≠ s.endPos) : pos.get h = s.str.toByteArray.utf8DecodeChar (s.startInclusive.offset.byteIdx + pos.offset.byteIdx) ⋯

theorem String.Slice.Pos.utf8Encode_get_eq_extract {s : Slice} (pos : s.Pos) (h : pos ≠ s.endPos) : [pos.get h].utf8Encode = s.str.toByteArray.extract (s.startInclusive.offset.byteIdx + pos.offset.byteIdx) (s.startInclusive.offset.byteIdx + pos.offset.byteIdx + (pos.get h).utf8Size)

def String.Slice.Pos.get? {s : Slice} (pos : s.Pos) : Option Char

Returns the byte at the given position in the string, or none if the position is the end position.

def String.Slice.Pos.get! {s : Slice} (pos : s.Pos) : Char

Returns the byte at the given position in the string, or panics if the position is the end position.

@[simp]

theorem String.Pos.Raw.isValidForSlice_toSlice_iff {s : String} {p : Raw} : IsValidForSlice s.toSlice p ↔ IsValid s p

theorem String.Pos.Raw.IsValid.toSlice {s : String} {p : Raw} (h : IsValid s p) : IsValidForSlice s.toSlice p

theorem String.Pos.Raw.IsValidForSlice.ofSlice {s : String} {p : Raw} (h : IsValidForSlice s.toSlice p) : IsValid s p

@[inline]

def String.Pos.toSlice {s : String} (pos : s.Pos) : s.toSlice.Pos

Turns a valid position on the string s into a valid position on the slice s.toSlice.

@[simp]

theorem String.Pos.offset_toSlice {s : String} {pos : s.Pos} : pos.toSlice.offset = pos.offset

@[inline]

def String.Pos.ofToSlice {s : String} (pos : s.toSlice.Pos) : s.Pos

Given a string s, turns a valid position on the slice s.toSlice into a valid position on the string s.

@[simp]

theorem String.Pos.offset_ofToSlice {s : String} {pos : s.toSlice.Pos} : (ofToSlice pos).offset = pos.offset

@[simp]

theorem String.rawEndPos_toSlice {s : String} : s.toSlice.rawEndPos = s.rawEndPos

@[simp]

theorem String.endPos_toSlice {s : String} : s.toSlice.endPos = s.endPos.toSlice

@[simp]

theorem String.startPos_toSlice {s : String} : s.toSlice.startPos = s.startPos.toSlice

@[simp]

theorem String.Pos.ofToSlice_toSlice {s : String} (pos : s.Pos) : ofToSlice pos.toSlice = pos

@[simp]

theorem String.Slice.Pos.toSlice_ofToSlice {s : String} (pos : s.toSlice.Pos) : (Pos.ofToSlice pos).toSlice = pos

@[simp]

theorem String.Pos.toSlice_comp_ofToSlice {s : String} : toSlice ∘ ofToSlice = id

@[simp]

theorem String.Pos.ofToSlice_comp_toSlice {s : String} : ofToSlice ∘ toSlice = id

theorem String.Pos.toSlice_inj {s : String} {p q : s.Pos} : p.toSlice = q.toSlice ↔ p = q

theorem String.Pos.ofToSlice_inj {s : String} {p q : s.toSlice.Pos} : ofToSlice p = ofToSlice q ↔ p = q

@[simp]

theorem String.Pos.toSlice_le {s : String} {p q : s.Pos} : p.toSlice ≤ q.toSlice ↔ p ≤ q

@[simp]

theorem String.Pos.ofToSlice_le {s : String} {p q : s.toSlice.Pos} : ofToSlice p ≤ ofToSlice q ↔ p ≤ q

@[simp]

theorem String.Pos.toSlice_lt {s : String} {p q : s.Pos} : p.toSlice < q.toSlice ↔ p < q

@[simp]

theorem String.Pos.ofToSlice_lt {s : String} {p q : s.toSlice.Pos} : ofToSlice p < ofToSlice q ↔ p < q

@[inline]

def String.Pos.get {s : String} (pos : s.Pos) (h : pos ≠ s.endPos) : Char

Returns the character at the position pos of a string, taking a proof that p is not the past-the-end position.

This function is overridden with an efficient implementation in runtime code.

Examples:

• ("abc".pos ⟨1⟩ (by decide)).get (by decide) = 'b'
• ("L∃∀N".pos ⟨1⟩ (by decide)).get (by decide) = '∃'

@[inline]

def String.Pos.get? {s : String} (pos : s.Pos) : Option Char

Returns the character at the position pos of a string, or none if the position is the past-the-end position.

This function is overridden with an efficient implementation in runtime code.

@[inline]

def String.Pos.get! {s : String} (pos : s.Pos) : Char

Returns the character at the position pos of a string, or panics if the position is the past-the-end position.

This function is overridden with an efficient implementation in runtime code.

@[inline]

def String.Pos.byte {s : String} (pos : s.Pos) (h : pos ≠ s.endPos) : UInt8

Returns the byte at the position pos of a string.

theorem String.Pos.isUTF8FirstByte_byte {s : String} {pos : s.Pos} {h : pos ≠ s.endPos} : (pos.byte h).IsUTF8FirstByte

@[simp]

theorem String.startPos_eq_endPos_iff {b : String} : b.startPos = b.endPos ↔ b = ""

theorem String.isSome_utf8DecodeChar?_zero {b : String} (hb : b ≠ "") : (b.toByteArray.utf8DecodeChar? 0).isSome = true

theorem String.head_toList {b : String} {h : b.toList ≠ []} : b.toList.head h = b.toByteArray.utf8DecodeChar 0 ⋯

@[deprecated String.head_toList (since := "2025-10-30")]

theorem String.head_data {b : String} {h : b.toList ≠ []} : b.toList.head h = b.toByteArray.utf8DecodeChar 0 ⋯

theorem String.get_startPos {b : String} (h : b.startPos ≠ b.endPos) : b.startPos.get h = b.toList.head ⋯

theorem String.eq_singleton_append {s : String} (h : s.startPos ≠ s.endPos) : ∃ (t : String), s = singleton (s.startPos.get h) ++ t

theorem String.Slice.copy_eq_copy_sliceTo {s : Slice} {pos : s.Pos} : s.copy = (s.sliceTo pos).copy ++ (s.sliceFrom pos).copy

@[inline]

def String.Pos.ofCopy {s : Slice} (pos : s.copy.Pos) : s.Pos

Given a slice s and a position on s.copy, obtain the corresponding position on s.

@[simp]

theorem String.Pos.offset_ofCopy {s : Slice} {pos : s.copy.Pos} : pos.ofCopy.offset = pos.offset

@[inline]

def String.Slice.Pos.copy {s : Slice} (pos : s.Pos) : s.copy.Pos

Given a slice s and a position on s, obtain the corresponding position on s.copy.

@[deprecated String.Slice.Pos.copy (since := "2025-12-01")]

def String.Slice.Pos.toCopy {s : Slice} (pos : s.Pos) : s.copy.Pos

@[simp]

theorem String.Slice.Pos.offset_copy {s : Slice} {pos : s.Pos} : pos.copy.offset = pos.offset

@[simp]

theorem String.Slice.Pos.ofCopy_copy {s : Slice} {pos : s.Pos} : pos.copy.ofCopy = pos

@[simp]

theorem String.Pos.copy_ofCopy {s : Slice} {pos : s.copy.Pos} : pos.ofCopy.copy = pos

theorem String.Pos.ofCopy_inj {s : Slice} {pos pos' : s.copy.Pos} : pos.ofCopy = pos'.ofCopy ↔ pos = pos'

@[simp]

theorem String.Slice.startPos_copy {s : Slice} : s.copy.startPos = s.startPos.copy

@[simp]

theorem String.Slice.endPos_copy {s : Slice} : s.copy.endPos = s.endPos.copy

theorem String.Slice.Pos.get_copy {s : Slice} {pos : s.Pos} (h : pos.copy ≠ s.copy.endPos) : pos.copy.get h = pos.get ⋯

theorem String.Slice.Pos.get_eq_get_copy {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos} : pos.get h = pos.copy.get ⋯

theorem String.Slice.Pos.byte_copy {s : Slice} {pos : s.Pos} (h : pos.copy ≠ s.copy.endPos) : pos.copy.byte h = pos.byte ⋯

theorem String.Slice.Pos.byte_eq_byte_copy {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos} : pos.byte h = pos.copy.byte ⋯

@[inline]

def String.Slice.Pos.ofSliceFrom {s : Slice} {p₀ : s.Pos} (pos : (s.sliceFrom p₀).Pos) : s.Pos

Given a position in s.sliceFrom p₀, obtain the corresponding position in s.

@[deprecated String.Slice.Pos.ofSliceFrom (since := "2025-11-20")]

def String.Slice.Pos.ofReplaceStart {s : Slice} {p₀ : s.Pos} (pos : (s.sliceFrom p₀).Pos) : s.Pos

@[simp]

theorem String.Slice.Pos.offset_ofSliceFrom {s : Slice} {p₀ : s.Pos} {pos : (s.sliceFrom p₀).Pos} : (ofSliceFrom pos).offset = pos.offset.offsetBy p₀.offset

@[inline]

def String.Slice.Pos.sliceFrom {s : Slice} (p₀ pos : s.Pos) (h : p₀ ≤ pos) : (s.sliceFrom p₀).Pos

Given a position in s that is at least p₀, obtain the corresponding position in s.sliceFrom p₀.

@[deprecated String.Slice.Pos.sliceFrom (since := "2025-11-20")]

def String.Slice.Pos.toReplaceStart {s : Slice} (p₀ pos : s.Pos) (h : p₀ ≤ pos) : (s.sliceFrom p₀).Pos

@[simp]

theorem String.Slice.Pos.offset_sliceFrom {s : Slice} {p₀ pos : s.Pos} {h : p₀ ≤ pos} : (p₀.sliceFrom pos h).offset = pos.offset.unoffsetBy p₀.offset

@[simp]

theorem String.Slice.Pos.ofSliceFrom_startPos {s : Slice} {pos : s.Pos} : ofSliceFrom (s.sliceFrom pos).startPos = pos

@[simp]

theorem String.Slice.Pos.ofSliceFrom_endPos {s : Slice} {pos : s.Pos} : ofSliceFrom (s.sliceFrom pos).endPos = s.endPos

theorem String.Slice.Pos.ofSliceFrom_inj {s : Slice} {p₀ : s.Pos} {pos pos' : (s.sliceFrom p₀).Pos} : ofSliceFrom pos = ofSliceFrom pos' ↔ pos = pos'

theorem String.Slice.Pos.get_eq_get_ofSliceFrom {s : Slice} {p₀ : s.Pos} {pos : (s.sliceFrom p₀).Pos} {h : pos ≠ (s.sliceFrom p₀).endPos} : pos.get h = (ofSliceFrom pos).get ⋯

@[inline]

def String.Slice.Pos.ofSliceTo {s : Slice} {p₀ : s.Pos} (pos : (s.sliceTo p₀).Pos) : s.Pos

Given a position in s.sliceTo p₀, obtain the corresponding position in s.

@[deprecated String.Slice.Pos.ofSliceTo (since := "2025-11-20")]

def String.Slice.Pos.ofReplaceEnd {s : Slice} {p₀ : s.Pos} (pos : (s.sliceTo p₀).Pos) : s.Pos

@[simp]

theorem String.Slice.Pos.offset_ofSliceTo {s : Slice} {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos} : (ofSliceTo pos).offset = pos.offset

@[inline]

def String.Slice.Pos.sliceTo {s : Slice} (p₀ pos : s.Pos) (h : pos ≤ p₀) : (s.sliceTo p₀).Pos

Given a position in s that is at most p₀, obtain the corresponding position in s.sliceTo p₀.

@[deprecated String.Slice.Pos.sliceTo (since := "2025-11-20")]

def String.Slice.Pos.toReplaceEnd {s : Slice} (p₀ pos : s.Pos) (h : pos ≤ p₀) : (s.sliceTo p₀).Pos

@[simp]

theorem String.Slice.Pos.offset_sliceTo {s : Slice} {p₀ pos : s.Pos} {h : pos ≤ p₀} : (p₀.sliceTo pos h).offset = pos.offset

theorem String.Slice.Pos.copy_eq_append_get {s : Slice} {pos : s.Pos} (h : pos ≠ s.endPos) : ∃ (t₁ : String), ∃ (t₂ : String), s.copy = t₁ ++ singleton (pos.get h) ++ t₂ ∧ t₁.utf8ByteSize = pos.offset.byteIdx

theorem String.Slice.Pos.utf8ByteSize_byte {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos} : (pos.byte h).utf8ByteSize ⋯ = (pos.get h).utf8Size

theorem String.Pos.utf8ByteSize_byte {s : String} {pos : s.Pos} {h : pos ≠ s.endPos} : (pos.byte h).utf8ByteSize ⋯ = (pos.get h).utf8Size

def String.Slice.Pos.next {s : Slice} (pos : s.Pos) (h : pos ≠ s.endPos) : s.Pos

Advances a valid position on a slice to the next valid position, given a proof that the position is not the past-the-end position, which guarantees that such a position exists.

def String.Slice.Pos.next? {s : Slice} (pos : s.Pos) : Option s.Pos

Advances a valid position on a slice to the next valid position, or returns none if the given position is the past-the-end position.

def String.Slice.Pos.next! {s : Slice} (pos : s.Pos) : s.Pos

Advances a valid position on a slice to the next valid position, or panics if the given position is the past-the-end position.

@[simp]

theorem String.Slice.Pos.offset_next {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos} : (pos.next h).offset = pos.offset + pos.get h

theorem String.Slice.Pos.byteIdx_offset_next {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos} : (pos.next h).offset.byteIdx = pos.offset.byteIdx + (pos.get h).utf8Size

@[simp]

theorem String.Slice.Pos.lt_next {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos} : pos < pos.next h

theorem String.Slice.Pos.copy_eq_copy_sliceTo_append_get {s : Slice} {pos : s.Pos} (h : pos ≠ s.endPos) : s.copy = (s.sliceTo pos).copy ++ singleton (pos.get h) ++ (s.sliceFrom (pos.next h)).copy

@[inline]

def String.Slice.Pos.prevAux {s : Slice} (pos : s.Pos) (h : pos ≠ s.startPos) : Pos.Raw

def String.Slice.Pos.prevAux.go {s : Slice} (off : Nat) (h₁ : off < s.utf8ByteSize) : Pos.Raw

theorem String.Pos.Raw.isValidForSlice_prevAuxGo {s : Slice} (off : Nat) (h₁ : off < s.utf8ByteSize) : IsValidForSlice s (Slice.Pos.prevAux.go off h₁)

theorem String.Pos.Raw.isValidForSlice_prevAux {s : Slice} (pos : s.Pos) (h : pos ≠ s.startPos) : IsValidForSlice s (pos.prevAux h)

@[inline]

def String.Slice.Pos.prev {s : Slice} (pos : s.Pos) (h : pos ≠ s.startPos) : s.Pos

Returns the previous valid position before the given position, given a proof that the position is not the start position, which guarantees that such a position exists.

def String.Slice.Pos.prev? {s : Slice} (pos : s.Pos) : Option s.Pos

Returns the previous valid position before the given position, or none if the position is the start position.

def String.Slice.Pos.prev! {s : Slice} (pos : s.Pos) : s.Pos

Returns the previous valid position before the given position, or panics if the position is the start position.

@[inline]

def String.Slice.pos (s : Slice) (off : Pos.Raw) (h : Pos.Raw.IsValidForSlice s off) : s.Pos

Constructs a valid position on s from a position and a proof that it is valid.

@[simp]

theorem String.Slice.offset_pos {s : Slice} {off : Pos.Raw} {h : Pos.Raw.IsValidForSlice s off} : (s.pos off h).offset = off

def String.Slice.pos? (s : Slice) (off : Pos.Raw) : Option s.Pos

Constructs a valid position on s from a position, returning none if the position is not valid.

def String.Slice.pos! (s : Slice) (off : Pos.Raw) : s.Pos

Constructs a valid position s from a position, panicking if the position is not valid.

@[extern lean_string_utf8_next_fast]

def String.Pos.next {s : String} (pos : s.Pos) (h : pos ≠ s.endPos) : s.Pos

Advances a valid position on a string to the next valid position, given a proof that the position is not the past-the-end position, which guarantees that such a position exists.

@[simp]

theorem String.Slice.Pos.str_inj {s : Slice} (p₁ p₂ : s.Pos) : p₁.str = p₂.str ↔ p₁ = p₂

@[inline]

def String.Pos.next? {s : String} (pos : s.Pos) : Option s.Pos

Advances a valid position on a string to the next valid position, or returns none if the given position is the past-the-end position.

@[inline]

def String.Pos.next! {s : String} (pos : s.Pos) : s.Pos

Advances a valid position on a string to the next valid position, or panics if the given position is the past-the-end position.

@[inline]

def String.Pos.prev {s : String} (pos : s.Pos) (h : pos ≠ s.startPos) : s.Pos

Returns the previous valid position before the given position, given a proof that the position is not the start position, which guarantees that such a position exists.

@[inline]

def String.Pos.prev? {s : String} (pos : s.Pos) : Option s.Pos

Returns the previous valid position before the given position, or none if the position is the start position.

@[inline]

def String.Pos.prev! {s : String} (pos : s.Pos) : s.Pos

Returns the previous valid position before the given position, or panics if the position is the start position.

@[inline]

def String.pos (s : String) (off : Pos.Raw) (h : Pos.Raw.IsValid s off) : s.Pos

Constructs a valid position on s from a position and a proof that it is valid.

@[inline]

def String.pos? (s : String) (off : Pos.Raw) : Option s.Pos

Constructs a valid position on s from a position, returning none if the position is not valid.

@[inline]

def String.pos! (s : String) (off : Pos.Raw) : s.Pos

Constructs a valid position s from a position, panicking if the position is not valid.

@[simp]

theorem String.offset_pos {s : String} {off : Pos.Raw} {h : Pos.Raw.IsValid s off} : (s.pos off h).offset = off

@[inline]

def String.Slice.Pos.cast {s t : Slice} (pos : s.Pos) (h : s = t) : t.Pos

Constructs a valid position on t from a valid position on s and a proof that s = t.

@[simp]

theorem String.Slice.Pos.offset_cast {s t : Slice} {pos : s.Pos} {h : s = t} : (pos.cast h).offset = pos.offset

@[simp]

theorem String.Slice.Pos.cast_rfl {s : Slice} {pos : s.Pos} : pos.cast ⋯ = pos

@[inline]

def String.Pos.cast {s t : String} (pos : s.Pos) (h : s = t) : t.Pos

Constructs a valid position on t from a valid position on s and a proof that s = t.

@[simp]

theorem String.Pos.offset_cast {s t : String} {pos : s.Pos} {h : s = t} : (pos.cast h).offset = pos.offset

@[simp]

theorem String.Pos.cast_rfl {s : String} {pos : s.Pos} : pos.cast ⋯ = pos

theorem String.Pos.copy_toSlice_eq_cast {s : String} (p : s.Pos) : p.toSlice.copy = p.cast ⋯

@[inline]

def String.Slice.findNextPos (offset : Pos.Raw) (s : Slice) (_h : offset < s.rawEndPos) : s.Pos

Given a byte position within a string slice, obtains the smallest valid position that is strictly greater than the given byte position.

theorem String.Slice.lt_offset_findNextPos {s : Slice} {o : Pos.Raw} (h : o < s.rawEndPos) : o < (findNextPos o s h).offset

theorem String.Slice.Pos.prevAuxGo_le_self {s : Slice} {p : Nat} {h : p < s.utf8ByteSize} : prevAux.go p h ≤ { byteIdx := p }

theorem String.Slice.Pos.prevAux_lt_self {s : Slice} {p : s.Pos} {h : p ≠ s.startPos} : p.prevAux h < p.offset

theorem String.Slice.Pos.prevAux_lt_rawEndPos {s : Slice} {p : s.Pos} {h : p ≠ s.startPos} : p.prevAux h < s.rawEndPos

@[simp]

theorem String.Slice.Pos.prev_ne_endPos {s : Slice} {p : s.Pos} {h : p ≠ s.startPos} : p.prev h ≠ s.endPos

@[simp]

theorem String.Pos.prev_ne_endPos {s : String} {p : s.Pos} {h : p ≠ s.startPos} : p.prev h ≠ s.endPos

theorem String.Pos.toSlice_prev {s : String} {p : s.Pos} {h : p ≠ s.startPos} : (p.prev h).toSlice = p.toSlice.prev ⋯

theorem String.Slice.Pos.offset_prev_lt_offset {s : Slice} {p : s.Pos} {h : p ≠ s.startPos} : (p.prev h).offset < p.offset

@[simp]

theorem String.Slice.Pos.prev_lt {s : Slice} {p : s.Pos} {h : p ≠ s.startPos} : p.prev h < p

@[simp]

theorem String.Pos.prev_lt {s : String} {p : s.Pos} {h : p ≠ s.startPos} : p.prev h < p

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

@[reducible, inline, deprecated String.Pos.Raw.utf8GetAux (since := "2025-10-09")]

abbrev String.utf8GetAux : List Char → Pos.Raw → Pos.Raw → Char

@[extern lean_string_utf8_get]

def String.Pos.Raw.get (s : String) (p : Raw) : 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.Pos.Raw.utf8GetAux for the reference implementation.

This is a legacy function. The recommended alternative is String.Pos.get, combined with String.pos or another means of obtaining a String.Pos.

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 '∃'.

@[extern lean_string_utf8_get, deprecated String.Pos.Raw.get (since := "2025-10-14")]

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

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

@[reducible, inline, deprecated String.Pos.Raw.utf8GetAux (since := "2025-10-09")]

abbrev String.utf8GetAux? : List Char → Pos.Raw → Pos.Raw → Option Char

@[extern lean_string_utf8_get_opt]

def String.Pos.Raw.get? : String → Raw → 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.

This is a legacy function. The recommended alternative is String.Pos.get, combined with String.pos? or another means of obtaining a String.Pos.

Examples:

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

@[extern lean_string_utf8_get_opt, deprecated String.Pos.Raw.get? (since := "2025-10-14")]

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

@[extern lean_string_utf8_get_bang]

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

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

See String.pos? and String.Pos.get for a safer alternative.

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

This is a legacy function. The recommended alternative is String.Pos.get, combined with String.pos! or another means of obtaining a String.Pos.

Examples

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

@[extern lean_string_utf8_get_bang, deprecated String.Pos.Raw.get! (since := "2025-10-14")]

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

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

@[reducible, inline, deprecated String.Pos.Raw.utf8SetAux (since := "2025-10-09")]

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

@[simp]

theorem String.Pos.get_toSlice {s : String} {p : s.Pos} {h : p.toSlice ≠ s.toSlice.endPos} : p.toSlice.get h = p.get ⋯

theorem String.Pos.get_eq_get_toSlice {s : String} {p : s.Pos} {h : p ≠ s.endPos} : p.get h = p.toSlice.get ⋯

@[simp]

theorem String.Pos.offset_next {s : String} (p : s.Pos) (h : p ≠ s.endPos) : (p.next h).offset = p.offset + p.get h

theorem String.Pos.byteIdx_offset_next {s : String} (p : s.Pos) (h : p ≠ s.endPos) : (p.next h).offset.byteIdx = p.offset.byteIdx + (p.get h).utf8Size

theorem String.Pos.toSlice_next {s : String} {p : s.Pos} {h : p ≠ s.endPos} : (p.next h).toSlice = p.toSlice.next ⋯

theorem String.Pos.byteIdx_lt_utf8ByteSize {s : String} (p : s.Pos) (h : p ≠ s.endPos) : p.offset.byteIdx < s.utf8ByteSize

@[simp]

theorem String.Pos.lt_next {s : String} {p : s.Pos} {h : p ≠ s.endPos} : p < p.next h

theorem String.Pos.ne_startPos_of_lt {s : String} {p q : s.Pos} : p < q → q ≠ s.startPos

theorem String.Pos.next_ne_startPos {s : String} {p : s.Pos} {h : p ≠ s.endPos} : p.next h ≠ s.startPos

@[simp]

theorem String.Pos.str_toSlice {s : String} {p : s.Pos} : p.toSlice.str = p

theorem String.Slice.Pos.str_le_endExclusive {s : Slice} (p : s.Pos) : p.str ≤ s.endExclusive

theorem String.Pos.lt_of_le_of_ne {s : String} {p q : s.Pos} : p ≤ q → p ≠ q → p < q

@[simp]

theorem String.Slice.Pos.str_endPos {s : Slice} : s.endPos.str = s.endExclusive

theorem String.Slice.Pos.str_lt_endExclusive {s : Slice} (p : s.Pos) (h : p ≠ s.endPos) : p.str < s.endExclusive

theorem String.Pos.ne_of_lt {s : String} {p q : s.Pos} : p < q → p ≠ q

theorem String.Pos.lt_of_lt_of_le {s : String} {p q r : s.Pos} : p < q → q ≤ r → p < r

theorem String.Pos.le_endPos {s : String} (p : s.Pos) : p ≤ s.endPos

theorem String.Slice.Pos.str_ne_endPos {s : Slice} (p : s.Pos) (h : p ≠ s.endPos) : p.str ≠ s.str.endPos

theorem String.Pos.le_trans {s : String} {p q r : s.Pos} : p ≤ q → q ≤ r → p ≤ r

theorem String.Pos.le_of_lt {s : String} {p q : s.Pos} : p < q → p ≤ q

theorem String.Slice.Pos.le_of_not_lt {s : Slice} {p q : s.Pos} : ¬q < p → p ≤ q

theorem String.Slice.Pos.ne_endPos_of_lt {s : Slice} {p q : s.Pos} : p < q → p ≠ s.endPos

theorem String.Slice.Pos.next_le_of_lt {s : Slice} {p q : s.Pos} {h : p ≠ s.endPos} : p < q → p.next h ≤ q

theorem String.Pos.ofToSlice_le_iff {s : String} {p : s.toSlice.Pos} {q : s.Pos} : ofToSlice p ≤ q ↔ p ≤ q.toSlice

@[simp]

theorem String.Pos.toSlice_lt_toSlice_iff {s : String} {p q : s.Pos} : p.toSlice < q.toSlice ↔ p < q

theorem String.Pos.next_le_of_lt {s : String} {p q : s.Pos} {h : p ≠ s.endPos} : p < q → p.next h ≤ q

theorem String.Slice.Pos.get_eq_get_str {s : Slice} {p : s.Pos} {h : p ≠ s.endPos} : p.get h = p.str.get ⋯

@[inline]

def String.Slice.Pos.nextFast {s : Slice} (pos : s.Pos) (h : pos ≠ s.endPos) : s.Pos

@[csimp]

theorem String.Slice.Pos.next_eq_nextFast : @next = @nextFast

@[inline]

def String.sliceTo (s : String) (p : s.Pos) : Slice

The slice from the beginning of s up to p (exclusive).

@[deprecated String.sliceTo (since := "2025-11-20")]

def String.replaceEnd (s : String) (p : s.Pos) : Slice

@[simp]

theorem String.str_sliceTo {s : String} {p : s.Pos} : (s.sliceTo p).str = s

@[simp]

theorem String.startInclusive_sliceTo {s : String} {p : s.Pos} : (s.sliceTo p).startInclusive = s.startPos

@[simp]

theorem String.endExclusive_sliceTo {s : String} {p : s.Pos} : (s.sliceTo p).endExclusive = p

@[simp]

theorem String.rawEndPos_sliceTo {s : String} {p : s.Pos} : (s.sliceTo p).rawEndPos = p.offset

theorem String.Pos.Raw.isValidForSlice_stringSliceTo {s : String} {p : s.Pos} {q : Raw} : IsValidForSlice (s.sliceTo p) q ↔ q ≤ p.offset ∧ IsValid s q

@[inline]

def String.sliceFrom (s : String) (p : s.Pos) : Slice

The slice from p (inclusive) up to the end of s.

@[deprecated String.sliceFrom (since := "2025-11-20")]

def String.replaceStart (s : String) (p : s.Pos) : Slice

@[simp]

theorem String.str_sliceFrom {s : String} {p : s.Pos} : (s.sliceFrom p).str = s

@[simp]

theorem String.startInclusive_sliceFrom {s : String} {p : s.Pos} : (s.sliceFrom p).startInclusive = p

@[simp]

theorem String.endExclusive_sliceFrom {s : String} {p : s.Pos} : (s.sliceFrom p).endExclusive = s.endPos

@[simp]

theorem String.utf8ByteSize_toSlice {s : String} : s.toSlice.utf8ByteSize = s.utf8ByteSize

@[simp]

theorem String.utf8ByteSize_sliceFrom {s : String} {p : s.Pos} : (s.sliceFrom p).utf8ByteSize = s.utf8ByteSize - p.offset.byteIdx

@[simp]

theorem String.utf8ByteSize_sliceTo {s : String} {p : s.Pos} : (s.sliceTo p).utf8ByteSize = p.offset.byteIdx

theorem String.Pos.Raw.isValidForSlice_stringSliceFrom {s : String} {p : s.Pos} {q : Raw} : IsValidForSlice (s.sliceFrom p) q ↔ IsValid s (q.offsetBy p.offset)

@[inline]

def String.slice (s : String) (startInclusive endExclusive : s.Pos) (h : startInclusive ≤ endExclusive) : Slice

Given a string and two valid positions within the string, obtain a slice on the string formed by the two positions.

This happens to be equivalent to the constructor of String.Slice.

@[simp]

theorem String.str_slice {s : String} {startInclusive endExclusive : s.Pos} {h : startInclusive ≤ endExclusive} : (s.slice startInclusive endExclusive h).str = s

@[simp]

theorem String.startInclusive_slice {s : String} {startInclusive endExclusive : s.Pos} {h : startInclusive ≤ endExclusive} : (s.slice startInclusive endExclusive h).startInclusive = startInclusive

@[simp]

theorem String.endExclusive_slice {s : String} {startInclusive endExclusive : s.Pos} {h : startInclusive ≤ endExclusive} : (s.slice startInclusive endExclusive h).endExclusive = endExclusive

def String.slice? (s : String) (startInclusive endExclusive : s.Pos) : Option Slice

Given a string and two valid positions within the string, obtain a slice on the string formed by the new bounds, or return none if the given end is strictly less then the given start.

def String.slice! (s : String) (p₁ p₂ : s.Pos) : Slice

Given a string and two valid positions within the string, obtain a slice on the string formed by the new bounds, or panic if the given end is strictly less than the given start.

@[deprecated String.slice! (since := "2025-11-20")]

def String.replaceStartEnd! (s : String) (p₁ p₂ : s.Pos) : Slice

theorem String.Pos.utf8Encode_get_eq_extract {s : String} (pos : s.Pos) (h : pos ≠ s.endPos) : [pos.get h].utf8Encode = s.toByteArray.extract pos.offset.byteIdx (pos.offset.byteIdx + (pos.get h).utf8Size)

theorem String.Pos.eq_copy_sliceTo_append_get {s : String} {pos : s.Pos} (h : pos ≠ s.endPos) : s = (s.sliceTo pos).copy ++ singleton (pos.get h) ++ (s.sliceFrom (pos.next h)).copy

@[inline]

def String.Pos.ofSliceFrom {s : String} {p₀ : s.Pos} (pos : (s.sliceFrom p₀).Pos) : s.Pos

Given a position in s.sliceFrom p₀, obtain the corresponding position in s.

@[deprecated String.Pos.ofSliceFrom (since := "2025-11-20")]

def String.Pos.ofReplaceStart {s : String} {p₀ : s.Pos} (pos : (s.sliceFrom p₀).Pos) : s.Pos

@[simp]

theorem String.Pos.offset_ofSliceFrom {s : String} {p₀ : s.Pos} {pos : (s.sliceFrom p₀).Pos} : (ofSliceFrom pos).offset = pos.offset.offsetBy p₀.offset

@[inline]

def String.Pos.sliceFrom {s : String} (p₀ pos : s.Pos) (h : p₀ ≤ pos) : (s.sliceFrom p₀).Pos

Given a position in s that is at least p₀, obtain the corresponding position in s.sliceFrom p₀.

@[deprecated String.Pos.sliceFrom (since := "2025-11-20")]

def String.Pos.toReplaceStart {s : String} (p₀ pos : s.Pos) (h : p₀ ≤ pos) : (s.sliceFrom p₀).Pos

@[simp]

theorem String.Pos.offset_sliceFrom {s : String} {p₀ pos : s.Pos} {h : p₀ ≤ pos} : (p₀.sliceFrom pos h).offset = pos.offset.unoffsetBy p₀.offset

@[simp]

theorem String.Pos.ofSliceFrom_startPos {s : String} {pos : s.Pos} : ofSliceFrom (s.sliceFrom pos).startPos = pos

@[simp]

theorem String.Pos.ofSliceFrom_endPos {s : String} {pos : s.Pos} : ofSliceFrom (s.sliceFrom pos).endPos = s.endPos

theorem String.Pos.ofSliceFrom_inj {s : String} {p₀ : s.Pos} {pos pos' : (s.sliceFrom p₀).Pos} : ofSliceFrom pos = ofSliceFrom pos' ↔ pos = pos'

@[simp]

theorem String.Pos.le_ofSliceFrom {s : String} {p₀ : s.Pos} {pos : (s.sliceFrom p₀).Pos} : p₀ ≤ ofSliceFrom pos

@[simp]

theorem String.Slice.Pos.le_ofSliceFrom {s : Slice} {p₀ : s.Pos} {pos : (s.sliceFrom p₀).Pos} : p₀ ≤ ofSliceFrom pos

theorem String.Pos.get_eq_get_ofSliceFrom {s : String} {p₀ : s.Pos} {pos : (s.sliceFrom p₀).Pos} {h : pos ≠ (s.sliceFrom p₀).endPos} : pos.get h = (ofSliceFrom pos).get ⋯

@[inline]

def String.Pos.ofSliceTo {s : String} {p₀ : s.Pos} (pos : (s.sliceTo p₀).Pos) : s.Pos

Given a position in s.sliceTo p₀, obtain the corresponding position in s.

@[deprecated String.Pos.ofSliceTo (since := "2025-11-20")]

def String.Pos.ofReplaceEnd {s : String} {p₀ : s.Pos} (pos : (s.sliceTo p₀).Pos) : s.Pos

@[simp]

theorem String.Pos.offset_ofSliceTo {s : String} {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos} : (ofSliceTo pos).offset = pos.offset

@[simp]

theorem String.Pos.ofSliceTo_le {s : String} {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos} : ofSliceTo pos ≤ p₀

@[simp]

theorem String.Slice.Pos.ofSliceTo_le {s : Slice} {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos} : ofSliceTo pos ≤ p₀

@[inline]

def String.Pos.sliceTo {s : String} (p₀ pos : s.Pos) (h : pos ≤ p₀) : (s.sliceTo p₀).Pos

Given a position in s that is at most p₀, obtain the corresponding position in s.sliceTo p₀.

@[deprecated String.Pos.sliceTo (since := "2025-11-20")]

def String.Pos.toReplaceEnd {s : String} (p₀ pos : s.Pos) (h : pos ≤ p₀) : (s.sliceTo p₀).Pos

@[simp]

theorem String.Pos.offset_sliceTo {s : String} {p₀ pos : s.Pos} {h : pos ≤ p₀} : (p₀.sliceTo pos h).offset = pos.offset

theorem String.Pos.Raw.isValidForSlice_slice {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} (pos : Raw) : IsValidForSlice (s.slice p₀ p₁ h) pos ↔ pos.offsetBy p₀.offset ≤ p₁.offset ∧ IsValidForSlice s (pos.offsetBy p₀.offset)

theorem String.Pos.Raw.isValidForSlice_stringSlice {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} (pos : Raw) : IsValidForSlice (s.slice p₀ p₁ h) pos ↔ pos.offsetBy p₀.offset ≤ p₁.offset ∧ IsValid s (pos.offsetBy p₀.offset)

@[inline]

def String.Slice.Pos.ofSlice {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} (pos : (s.slice p₀ p₁ h).Pos) : s.Pos

Given a position in s.slice p₀ p₁ h, obtain the corresponding position in s.

@[simp]

theorem String.Slice.Pos.offset_ofSlice {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {pos : (s.slice p₀ p₁ h).Pos} : (ofSlice pos).offset = pos.offset.offsetBy p₀.offset

@[inline]

def String.Pos.ofSlice {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} (pos : (s.slice p₀ p₁ h).Pos) : s.Pos

Given a position in s.slice p₀ p₁ h, obtain the corresponding position in s.

@[simp]

theorem String.Pos.offset_ofSlice {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {pos : (s.slice p₀ p₁ h).Pos} : (ofSlice pos).offset = pos.offset.offsetBy p₀.offset

theorem String.Slice.Pos.le_trans {s : Slice} {p q r : s.Pos} : p ≤ q → q ≤ r → p ≤ r

@[inline]

def String.Slice.Pos.slice {s : Slice} (pos p₀ p₁ : s.Pos) (h₁ : p₀ ≤ pos) (h₂ : pos ≤ p₁) : (s.slice p₀ p₁ ⋯).Pos

Given a position in s that is between p₀ and p₁, obtain the corresponding position in s.slice p₀ p₁ h.

@[inline]

def String.Pos.slice {s : String} (pos p₀ p₁ : s.Pos) (h₁ : p₀ ≤ pos) (h₂ : pos ≤ p₁) : (s.slice p₀ p₁ ⋯).Pos

Given a position in s that is between p₀ and p₁, obtain the corresponding position in s.slice p₀ p₁ h.

@[simp]

theorem String.Pos.offset_slice {s : String} {p₀ p₁ pos : s.Pos} {h₁ : p₀ ≤ pos} {h₂ : pos ≤ p₁} : (pos.slice p₀ p₁ h₁ h₂).offset = pos.offset.unoffsetBy p₀.offset

@[inline]

def String.Slice.Pos.sliceOrPanic {s : Slice} (pos p₀ p₁ : s.Pos) {h : p₀ ≤ p₁} : (s.slice p₀ p₁ h).Pos

Given a position in s, obtain the corresponding position in s.slice p₀ p₁ h, or panic if pos is not between p₀ and p₁.

@[inline]

def String.Pos.sliceOrPanic {s : String} (pos p₀ p₁ : s.Pos) {h : p₀ ≤ p₁} : (s.slice p₀ p₁ h).Pos

Given a position in s, obtain the corresponding position in s.slice p₀ p₁ h, or panic if pos is not between p₀ and p₁.

theorem String.Slice.slice_eq_slice! {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} : s.slice p₀ p₁ h = s.slice! p₀ p₁

theorem String.slice_eq_slice! {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} : s.slice p₀ p₁ h = s.slice! p₀ p₁

@[inline]

def String.Slice.Pos.ofSlice! {s : Slice} {p₀ p₁ : s.Pos} (pos : (s.slice! p₀ p₁).Pos) : s.Pos

Given a position in s.slice! p₀ p₁, obtain the corresponding position in s, or panic if taking s.slice! p₀ p₁ already panicked.

@[inline]

def String.Pos.ofSlice! {s : String} {p₀ p₁ : s.Pos} (pos : (s.slice! p₀ p₁).Pos) : s.Pos

Given a position in s.slice! p₀ p₁, obtain the corresponding position in s, or panic if taking s.slice! p₀ p₁ already panicked.

@[inline]

def String.Slice.Pos.slice! {s : Slice} (pos p₀ p₁ : s.Pos) : (s.slice! p₀ p₁).Pos

Given a position in s, obtain the corresponding position in s.slice! p₀ p₁ h, or panic if taking s.slice! p₀ p₁ already panicked or if the position is not between p₀ and p₁.

@[inline]

def String.Pos.slice! {s : String} (pos p₀ p₁ : s.Pos) : (s.slice! p₀ p₁).Pos

Given a position in s, obtain the corresponding position in s.slice! p₀ p₁ h, or panic if taking s.slice! p₀ p₁ already panicked or if the position is not between p₀ and p₁.

theorem String.extract_eq_copy_slice {s : String} (p₀ p₁ : s.Pos) (h : p₀ ≤ p₁) : extract p₀ p₁ = (s.slice p₀ p₁ h).copy

@[inline]

def String.Slice.extract (s : Slice) (p₀ p₁ : s.Pos) : String

Copies a region of a slice to a new string.

The region of s from b (inclusive) to e (exclusive) is copied to a newly-allocated String.

If b's offset is greater than or equal to that of e, then the resulting string is "".

If possible, prefer Slice.slice, which avoids the allocation.

@[simp]

theorem String.Slice.Pos.str_le_str_iff {s : Slice} {p q : s.Pos} : p.str ≤ q.str ↔ p ≤ q

@[simp]

theorem String.Slice.Pos.str_lt_str_iff {s : Slice} {p q : s.Pos} : p.str < q.str ↔ p < q

theorem String.Slice.extract_eq_copy_slice {s : Slice} (p₀ p₁ : s.Pos) (h : p₀ ≤ p₁) : s.extract p₀ p₁ = (s.slice p₀ p₁ h).copy

def String.Slice.Pos.nextn {s : Slice} (p : s.Pos) (n : Nat) : s.Pos

Advances the position p n times.

If this would move p past the end of s, the result is s.endPos.

def String.Slice.Pos.prevn {s : Slice} (p : s.Pos) (n : Nat) : s.Pos

Iterates p.prev n times.

If this would move p past the start of s, the result is s.endPos.

@[inline]

def String.Pos.nextn {s : String} (p : s.Pos) (n : Nat) : s.Pos

Advances the position p n times.

If this would move p past the end of s, the result is s.endPos.

@[inline]

def String.Pos.prevn {s : String} (p : s.Pos) (n : Nat) : s.Pos

Iterates p.prev n times.

If this would move p past the start of s, the result is s.startPos.

theorem String.Slice.Pos.le_nextn {s : Slice} {p : s.Pos} {n : Nat} : p ≤ p.nextn n

theorem String.Pos.le_nextn {s : String} {p : s.Pos} {n : Nat} : p ≤ p.nextn n

theorem String.Slice.Pos.prevn_le {s : Slice} {p : s.Pos} {n : Nat} : p.prevn n ≤ p

theorem String.Pos.prevn_le {s : String} {p : s.Pos} {n : Nat} : p.prevn n ≤ p

@[extern lean_string_utf8_next]

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

Returns the next position in a string after position p. If p is not a valid position or p = s.endPos, returns the position one byte after p.

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.

This is a legacy function. The recommended alternative is String.Pos.next or one of its variants like String.Pos.next?, combined with String.pos or another means of obtaining a String.ValisPos.

Some examples of edge cases:

• "abc".next ⟨3⟩ = ⟨4⟩, since 3 = "abc".endPos
• "L∃∀N".next ⟨2⟩ = ⟨3⟩, 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) = '∀'

@[extern lean_string_utf8_next, deprecated String.Pos.Raw.next (since := "2025-10-14")]

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

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

@[reducible, inline, deprecated String.Pos.Raw.utf8PrevAux (since := "2025-10-10")]

abbrev String.utf8PrevAux : List Char → Pos.Raw → Pos.Raw → Pos.Raw

@[extern lean_string_utf8_prev]

def String.Pos.Raw.prev : String → Raw → Raw

Returns the position in a string before a specified position, p. If p = ⟨0⟩, returns 0. If p is greater than rawEndPos, returns the position one byte before p. Otherwise, if p occurs in the middle of a multi-byte character, returns the beginning position of that character.

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

This is a legacy function. The recommended alternative is String.Pos.prev or one of its variants like String.Pos.prev?, combined with String.pos or another means of obtaining a String.Pos.

Examples:

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

@[extern lean_string_utf8_prev, deprecated String.Pos.Raw.prev (since := "2025-10-14")]

def String.prev : String → Pos.Raw → Pos.Raw

@[extern lean_string_utf8_at_end]

def String.Pos.Raw.atEnd : String → Raw → 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

@[extern lean_string_utf8_at_end, deprecated String.Pos.Raw.atEnd (since := "2025-10-14")]

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

@[extern lean_string_utf8_get_fast]

def String.Pos.Raw.get' (s : String) (p : Raw) (h : ¬atEnd s 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).

This is a legacy function. The recommended alternative is String.Pos.get, combined with String.pos or another means of obtaining a String.Pos.

Examples:

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

@[extern lean_string_utf8_get_fast, deprecated String.Pos.Raw.get' (since := "2025-10-14")]

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

@[extern lean_string_utf8_next_fast]

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

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)

This is a legacy function. The recommended alternative is String.Pos.next, combined with String.pos or another means of obtaining a String.Pos.

Example:

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

@[extern lean_string_utf8_next_fast, deprecated String.Pos.Raw.next' (since := "2025-10-14")]

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

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

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

@[deprecated String.Pos.Raw.byteIdx_lt_byteIdx_next (since := "2025-10-10")]

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

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

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

@[deprecated String.Pos.Raw.prev_lt_of_pos (since := "2025-10-10")]

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

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

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⟩

@[irreducible]

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

@[extern lean_string_utf8_extract]

def String.Pos.Raw.extract : String → Raw → Raw → 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.

This is a legacy function. The recommended alternative is String.Pos.extract, but usually it is even better to operate on String.Slice instead and call String.Slice.copy (only) if required.

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 ⟨1⟩ ⟨2⟩ = "∃∀N"
• "L∃∀N".extract ⟨2⟩ ⟨100⟩ = ""

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

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

@[irreducible]

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

@[inline]

def String.Pos.Raw.offsetOfPos (s : String) (pos : Raw) : 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

@[deprecated String.Pos.Raw.offsetOfPos (since := "2025-11-17")]

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

@[export lean_string_offsetofpos]

def String.Internal.offsetOfPosImpl (s : String) (pos : Pos.Raw) : Nat

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

def String.Pos.Raw.substrEq (s1 : String) (pos1 : Raw) (s2 : String) (pos2 : Raw) (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.

This is a legacy function. The recommended alternative is to construct slices representing the strings to be compared and use the BEq instance of String.Slice.

@[deprecated String.Pos.Raw.substrEq (since := "2025-10-10")]

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

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

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

@[simp]

theorem String.length_empty : "".length = 0

@[deprecated String.singleton_eq_ofList (since := "2025-10-30")]

theorem String.singleton_eq {c : Char} : singleton c = ofList [c]

@[simp]

theorem String.toList_singleton (c : Char) : (singleton c).toList = [c]

@[deprecated String.toList_singleton (since := "2025-10-30")]

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

@[simp]

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

@[simp]

theorem String.toList_push {s : String} (c : Char) : (s.push c).toList = s.toList ++ [c]

@[deprecated String.toList_push (since := "2025-10-30")]

theorem String.data_push {s : String} (c : Char) : (s.push c).toList = s.toList ++ [c]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[deprecated String.Pos.Raw.get!_eq_get (since := "2025-10-14")]

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

@[deprecated String.Pos.Raw.lt_next (since := "2025-10-10")]

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

@[simp]

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

@[deprecated String.Pos.Raw.prev_zero (since := "2025-10-10")]

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

@[deprecated String.Pos.Raw.get'_eq (since := "2025-10-14")]

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

@[deprecated String.Pos.Raw.next'_eq (since := "2025-10-14")]

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

@[deprecated String.size_toByteArray (since := "2025-11-24")]

theorem String.size_bytes {s : String} : s.toByteArray.size = s.utf8ByteSize

@[deprecated String.toByteArray_ofList (since := "2025-11-24")]

theorem String.bytes_ofList {l : List Char} : (ofList l).toByteArray = l.utf8Encode

@[deprecated String.toByteArray_inj (since := "2025-11-24")]

theorem String.bytes_inj {s t : String} : s.toByteArray = t.toByteArray ↔ s = t

@[simp]

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