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.

Equations

• b.utf8Decode? = ByteArray.utf8Decode?.go b 0 #[] ⋯

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

Equations

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

@[extern lean_string_validate_utf8]

def ByteArray.validateUTF8 (b : ByteArray) : Bool

Equations

• b.validateUTF8 = ByteArray.validateUTF8.go b 0 ⋯

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

Equations

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

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

Equations

• instDecidableIsValidUTF8 = decidable_of_iff (b.validateUTF8 = true) ⋯

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

Equations

• String.fromUTF8? a = if h : a.IsValidUTF8 then some (String.fromUTF8 a h) else none

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

Equations

• String.fromUTF8! a = if h : a.IsValidUTF8 then String.fromUTF8 a h else panicWithPosWithDecl "Init.Data.String.Basic" "String.fromUTF8!" 185 46 "invalid UTF-8 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

Equations

• String.Internal.toArray b = b.toByteArray.utf8Decode?.get ⋯

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

Equations

• s.toList = (String.Internal.toArray s).toList

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

Equations

• b.data = (String.Internal.toArray b).toList

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

Equations

• b.length = b.toList.length

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

Equations

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

@[extern lean_string_dec_lt]

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

Equations

• s₁.decidableLT s₂ = s₁.toList.decidableLT s₂.toList

@[reducible]

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

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

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

Equations

• a.le b = ¬b < a

instance String.instLE : LE String

Equations

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

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

Equations

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

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

Equations

• String.Pos.Raw.isValid s p = if h : p < s.rawEndPos then decide (s.getUTF8Byte p h).IsUTF8FirstByte else decide (p = s.rawEndPos)

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

Equations

• String.instDecidableIsValid = decidable_of_iff (String.Pos.Raw.isValid s p = true) ⋯

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.

Equations

• String.extract b e = { toByteArray := s.toByteArray.extract b.offset.byteIdx e.offset.byteIdx, isValidUTF8 := ⋯ }

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

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

Equations

• b.extract e = String.extract b e

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

Equations

• s.copy = String.extract s.startInclusive s.endExclusive

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.

Equations

• String.Pos.Raw.isValidForSlice s p = if h : p < s.rawEndPos then decide (s.getUTF8Byte p h).IsUTF8FirstByte else decide (p = s.rawEndPos)

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

Equations

• String.instDecidableIsValidForSlice = decidable_of_iff (String.Pos.Raw.isValidForSlice s p = true) ⋯

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.

Equations

• pos.str = { offset := pos.offset.offsetBy s.startInclusive.offset, isValid := ⋯ }

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

Equations

• String.Slice.Pos.ofStr pos h₁ h₂ = { offset := pos.offset.unoffsetBy s.startInclusive.offset, isValidForSlice := ⋯ }

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

Equations

• s.sliceFrom pos = { str := s.str, startInclusive := pos.str, endExclusive := s.endExclusive, startInclusive_le_endExclusive := ⋯ }

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

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

Equations

• s.replaceStart pos = s.sliceFrom pos

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

Equations

• s.sliceTo pos = { str := s.str, startInclusive := s.startInclusive, endExclusive := pos.str, startInclusive_le_endExclusive := ⋯ }

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

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

Equations

• s.replaceEnd pos = s.sliceTo pos

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

Equations

• s.slice newStart newEnd h = { str := s.str, startInclusive := newStart.str, endExclusive := newEnd.str, startInclusive_le_endExclusive := ⋯ }

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

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

Equations

• s.replaceStartEnd newStart newEnd h = s.slice newStart newEnd h

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

Equations

• s.slice? newStart newEnd = if h : newStart.offset ≤ newEnd.offset then some (s.slice newStart newEnd h) else none

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.

Equations

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

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

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

Equations

• s.replaceStartEnd! newStart newEnd = s.slice! newStart newEnd

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

Equations

• s.decodeChar byteIdx h = s.toByteArray.utf8DecodeChar byteIdx h

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

Equations

• pos.get h = s.str.decodeChar (s.startInclusive.offset.byteIdx + pos.offset.byteIdx) ⋯

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.

Equations

• pos.get? = if h : pos = s.endPos then none else some (pos.get h)

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.

Equations

• pos.get! = if h : pos = s.endPos then panicWithPosWithDecl "Init.Data.String.Basic" "String.Slice.Pos.get!" 1184 29 "Cannot retrieve character at end position" else pos.get h

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

Equations

• pos.toSlice = { offset := pos.offset, isValidForSlice := ⋯ }

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

Equations

• String.Pos.ofToSlice pos = { offset := pos.offset, isValid := ⋯ }

@[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) = '∃'

Equations

• pos.get h = pos.toSlice.get ⋯

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

Equations

• pos.get? = pos.toSlice.get?

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

Equations

• pos.get! = pos.toSlice.get!

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

Equations

• pos.byte h = pos.toSlice.byte ⋯

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.

Equations

• pos.ofCopy = { offset := pos.offset, isValidForSlice := ⋯ }

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

Equations

• pos.copy = { offset := pos.offset, isValid := ⋯ }

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

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

Equations

• pos.toCopy = pos.copy

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

Equations

• String.Slice.Pos.ofSliceFrom pos = { offset := pos.offset.offsetBy p₀.offset, isValidForSlice := ⋯ }

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

Equations

• String.Slice.Pos.ofReplaceStart pos = String.Slice.Pos.ofSliceFrom 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₀.

Equations

• p₀.sliceFrom pos h = { offset := pos.offset.unoffsetBy p₀.offset, isValidForSlice := ⋯ }

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

Equations

• p₀.toReplaceStart pos h = p₀.sliceFrom pos h

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

Equations

• String.Slice.Pos.ofSliceTo pos = { offset := pos.offset, isValidForSlice := ⋯ }

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

Equations

• String.Slice.Pos.ofReplaceEnd pos = String.Slice.Pos.ofSliceTo 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₀.

Equations

• p₀.sliceTo pos h = { offset := pos.offset, isValidForSlice := ⋯ }

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

Equations

• p₀.toReplaceEnd pos h = p₀.sliceTo pos h

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

Equations

• pos.next h = { offset := pos.offset.increaseBy ((pos.byte h).utf8ByteSize ⋯), isValidForSlice := ⋯ }

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.

Equations

• pos.next? = if h : pos = s.endPos then none else some (pos.next h)

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.

Equations

• pos.next! = if h : pos = s.endPos then panicWithPosWithDecl "Init.Data.String.Basic" "String.Slice.Pos.next!" 1544 29 "Cannot advance the end position" else pos.next h

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

Equations

• pos.prevAux h = String.Slice.Pos.prevAux.go (pos.offset.byteIdx - 1) ⋯

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

Equations

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

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.

Equations

• pos.prev h = { offset := pos.prevAux h, isValidForSlice := ⋯ }

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.

Equations

• pos.prev? = if h : pos = s.startPos then none else some (pos.prev h)

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.

Equations

• pos.prev! = if h : pos = s.startPos then panicWithPosWithDecl "Init.Data.String.Basic" "String.Slice.Pos.prev!" 1626 31 "The start position has no previous position" else pos.prev h

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

Equations

• s.pos off h = { offset := off, isValidForSlice := h }

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

Equations

• s.pos? off = if h : String.Pos.Raw.isValidForSlice s off = true then some (s.pos off ⋯) else none

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.

Equations

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

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

Equations

• pos.next h = String.Pos.ofToSlice (pos.toSlice.next ⋯)

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

Equations

• pos.next? = Option.map String.Pos.ofToSlice pos.toSlice.next?

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

Equations

• pos.next! = String.Pos.ofToSlice pos.toSlice.next!

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

Equations

• pos.prev h = String.Pos.ofToSlice (pos.toSlice.prev ⋯)

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

Equations

• pos.prev? = Option.map String.Pos.ofToSlice pos.toSlice.prev?

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

Equations

• pos.prev! = String.Pos.ofToSlice pos.toSlice.prev!

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

Equations

• s.pos off h = String.Pos.ofToSlice (s.toSlice.pos off ⋯)

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

Equations

• s.pos? off = Option.map String.Pos.ofToSlice (s.toSlice.pos? off)

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

Equations

• s.pos! off = String.Pos.ofToSlice (s.toSlice.pos! off)

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

Equations

• pos.cast h = { offset := pos.offset, isValidForSlice := ⋯ }

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

Equations

• pos.cast h = { offset := pos.offset, isValid := ⋯ }

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

Equations

• String.Slice.findNextPos offset s _h = String.Slice.findNextPos.go✝ s offset.inc

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

Equations

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

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

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

Equations

• String.utf8GetAux = String.Pos.Raw.utf8GetAux

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

Equations

• String.Pos.Raw.get s p = String.Pos.Raw.utf8GetAux s.toList 0 p

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

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

Equations

• s.get p = String.Pos.Raw.utf8GetAux s.toList 0 p

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

Equations

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

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

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

Equations

• String.utf8GetAux? = String.Pos.Raw.utf8GetAux?

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

Equations

• String.Pos.Raw.get? x✝¹ x✝ = String.Pos.Raw.utf8GetAux? x✝¹.toList 0 x✝

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

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

Equations

• x✝¹.get? x✝ = String.Pos.Raw.utf8GetAux? x✝¹.toList 0 x✝

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

Equations

• String.Pos.Raw.get! s p = String.Pos.Raw.utf8GetAux s.toList 0 p

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

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

Equations

• s.get! p = String.Pos.Raw.utf8GetAux s.toList 0 p

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

Equations

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

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

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

Equations

• String.utf8SetAux c' = String.Pos.Raw.utf8SetAux c'

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

Equations

• pos.nextFast h = String.Slice.Pos.ofStr (pos.str.next ⋯) ⋯ ⋯

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

Equations

• s.sliceTo p = s.toSlice.sliceTo p.toSlice

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

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

Equations

• s.replaceEnd p = s.sliceTo p

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

Equations

• s.sliceFrom p = s.toSlice.sliceFrom p.toSlice

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

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

Equations

• s.replaceStart p = s.sliceFrom p

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

Equations

• s.slice startInclusive endExclusive h = s.toSlice.slice startInclusive.toSlice endExclusive.toSlice ⋯

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

Equations

• s.slice? startInclusive endExclusive = if h : startInclusive ≤ endExclusive then some (s.slice startInclusive endExclusive h) else none

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.

Equations

• s.slice! p₁ p₂ = s.toSlice.slice! p₁.toSlice p₂.toSlice

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

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

Equations

• s.replaceStartEnd! p₁ p₂ = s.slice! p₁ p₂

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.

Equations

• String.Pos.ofSliceFrom pos = { offset := pos.offset.offsetBy p₀.offset, isValid := ⋯ }

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

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

Equations

• String.Pos.ofReplaceStart pos = String.Pos.ofSliceFrom 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₀.

Equations

• p₀.sliceFrom pos h = { offset := pos.offset.unoffsetBy p₀.offset, isValidForSlice := ⋯ }

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

Equations

• p₀.toReplaceStart pos h = p₀.sliceFrom pos h

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

Equations

• String.Pos.ofSliceTo pos = { offset := pos.offset, isValid := ⋯ }

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

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

Equations

• String.Pos.ofReplaceEnd pos = String.Pos.ofSliceTo 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₀.

Equations

• p₀.sliceTo pos h = { offset := pos.offset, isValidForSlice := ⋯ }

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

Equations

• p₀.toReplaceEnd pos h = p₀.sliceTo pos h

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

Equations

• String.Slice.Pos.ofSlice pos = { offset := pos.offset.offsetBy p₀.offset, isValidForSlice := ⋯ }

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

Equations

• String.Pos.ofSlice pos = String.Pos.ofToSlice (String.Slice.Pos.ofSlice pos)

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

Equations

• pos.slice p₀ p₁ h₁ h₂ = { offset := pos.offset.unoffsetBy p₀.offset, isValidForSlice := ⋯ }

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

Equations

• pos.slice p₀ p₁ h₁ h₂ = pos.toSlice.slice p₀.toSlice p₁.toSlice h₁ 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₁.

Equations

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

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

Equations

• pos.sliceOrPanic p₀ p₁ = pos.toSlice.sliceOrPanic p₀.toSlice p₁.toSlice

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.

Equations

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

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

Equations

• String.Pos.ofSlice! pos = String.Pos.ofToSlice (String.Slice.Pos.ofSlice! pos)

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

Equations

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

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

Equations

• pos.slice! p₀ p₁ = pos.toSlice.slice! p₀.toSlice p₁.toSlice

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.

Equations

• s.extract p₀ p₁ = String.extract p₀.str p₁.str

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

Equations

• p.nextn 0 = p
• p.nextn n_2.succ = if h : p ≠ s.endPos then (p.next h).nextn n_2 else p

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.

Equations

• p.prevn 0 = p
• p.prevn n_2.succ = if h : p ≠ s.startPos then (p.prev h).prevn n_2 else p

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

Equations

• p.nextn n = String.Pos.ofToSlice (p.toSlice.nextn n)

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

Equations

• p.prevn n = String.Pos.ofToSlice (p.toSlice.prevn n)

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) = '∀'

Equations

• String.Pos.Raw.next s p = p + String.Pos.Raw.get s p

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

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

Equations

• s.next p = p + String.Pos.Raw.get s p

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

Equations

• String.Pos.Raw.utf8PrevAux [] x✝¹ x✝ = { byteIdx := x✝.byteIdx - 1 }
• String.Pos.Raw.utf8PrevAux (c :: cs) x✝¹ x✝ = if x✝ ≤ x✝¹ + c then x✝¹ else String.Pos.Raw.utf8PrevAux cs (x✝¹ + c) x✝

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

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

Equations

• String.utf8PrevAux = String.Pos.Raw.utf8PrevAux

@[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) = '∃'

Equations

• String.Pos.Raw.prev x✝¹ x✝ = String.Pos.Raw.utf8PrevAux x✝¹.toList 0 x✝

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

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

Equations

• x✝¹.prev x✝ = String.Pos.Raw.utf8PrevAux x✝¹.toList 0 x✝

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

Equations

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

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

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

Equations

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

@[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) = '∀'

Equations

• String.Pos.Raw.get' s p h = String.Pos.Raw.utf8GetAux s.toList 0 p

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

Equations

• s.get' p h = String.Pos.Raw.utf8GetAux s.toList 0 p

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

Equations

• String.Pos.Raw.next' s p h = p + String.Pos.Raw.get s p

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

Equations

• s.next' p h = p + String.Pos.Raw.get s p

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⟩

Equations

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

@[irreducible]

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

Equations

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

@[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⟩ = ""

Equations

• String.Pos.Raw.extract x✝² x✝¹ x✝ = if x✝¹.byteIdx ≥ x✝.byteIdx then "" else String.ofList (String.Pos.Raw.extract.go₁ x✝².toList 0 x✝¹ x✝)

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

Equations

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

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

Equations

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

@[irreducible]

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

Equations

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

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

Equations

• String.Pos.Raw.offsetOfPos s pos = String.Pos.Raw.offsetOfPosAux s pos 0 0

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

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

Equations

• s.offsetOfPos pos = String.Pos.Raw.offsetOfPos s pos

@[export lean_string_offsetofpos]

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

Equations

• String.Internal.offsetOfPosImpl s pos = String.Pos.Raw.offsetOfPos s pos

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.

Equations

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

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

Equations

• s1.substrEq pos1 s2 pos2 sz = String.Pos.Raw.substrEq s1 pos1 s2 pos2 sz

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