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 (b.size + 1) 0 #[] ⋯ ⋯

def ByteArray.utf8Decode?.go (b : ByteArray) (fuel i : Nat) (acc : Array Char) (hi : i ≤ b.size) (hf : b.size - i < fuel) : 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 (b.size + 1) 0 ⋯ ⋯

def ByteArray.validateUTF8.go (b : ByteArray) (fuel i : Nat) (hi : i ≤ b.size) (hf : b.size - i < fuel) : Bool

Equations

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

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

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

theorem ByteArray.utf8Decode?.go.congr {b b' : ByteArray} {fuel fuel' i i' : Nat} {acc acc' : Array Char} {hi : i ≤ b.size} {hi' : i' ≤ b'.size} {hf : b.size - i < fuel} {hf' : b'.size - i' < fuel'} (hbb' : b = b') (hii' : i = i') (hacc : acc = acc') : go b fuel i acc hi hf = go b' fuel' i' acc' hi' hf'

@[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!" 212 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.bytes.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.bytes

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

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

@[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.bytes.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.bytes.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.bytes.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.bytes.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.bytes.extract p.byteIdx s.utf8ByteSize).IsValidUTF8

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

@[extern lean_string_utf8_extract]

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

Equations

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

@[inline]

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

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

Equations

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

theorem String.Slice.bytes_copy {s : Slice} : s.copy.bytes = s.str.bytes.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.bytes.utf8DecodeChar? p.byteIdx).isSome = true

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

theorem String.Pos.Raw.isValidForSlice_iff_isSome_utf8DecodeChar? {s : Slice} {p : Raw} : IsValidForSlice s p ↔ p = s.rawEndPos ∨ p < s.rawEndPos ∧ (s.str.bytes.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.ValidPos

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

@[inline]

def String.Slice.replaceStart (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.replaceStart pos = { str := s.str, startInclusive := pos.str, endExclusive := s.endExclusive, startInclusive_le_endExclusive := ⋯ }

@[simp]

theorem String.Slice.str_replaceStart {s : Slice} {pos : s.Pos} : (s.replaceStart pos).str = s.str

@[simp]

theorem String.Slice.startInclusive_replaceStart {s : Slice} {pos : s.Pos} : (s.replaceStart pos).startInclusive = pos.str

@[simp]

theorem String.Slice.endExclusive_replaceStart {s : Slice} {pos : s.Pos} : (s.replaceStart pos).endExclusive = s.endExclusive

@[inline]

def String.Slice.replaceEnd (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.replaceEnd pos = { str := s.str, startInclusive := s.startInclusive, endExclusive := pos.str, startInclusive_le_endExclusive := ⋯ }

@[simp]

theorem String.Slice.str_replaceEnd {s : Slice} {pos : s.Pos} : (s.replaceEnd pos).str = s.str

@[simp]

theorem String.Slice.startInclusive_replaceEnd {s : Slice} {pos : s.Pos} : (s.replaceEnd pos).startInclusive = s.startInclusive

@[simp]

theorem String.Slice.endExclusive_replaceEnd {s : Slice} {pos : s.Pos} : (s.replaceEnd pos).endExclusive = pos.str

@[inline]

def String.Slice.replaceStartEnd (s : Slice) (newStart newEnd : s.Pos) (h : newStart.offset ≤ newEnd.offset) : 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.replaceStartEnd newStart newEnd h = { str := s.str, startInclusive := newStart.str, endExclusive := newEnd.str, startInclusive_le_endExclusive := ⋯ }

@[simp]

theorem String.Slice.str_replaceStartEnd {s : Slice} {newStart newEnd : s.Pos} {h : newStart.offset ≤ newEnd.offset} : (s.replaceStartEnd newStart newEnd h).str = s.str

@[simp]

theorem String.Slice.startInclusive_replaceStartEnd {s : Slice} {newStart newEnd : s.Pos} {h : newStart.offset ≤ newEnd.offset} : (s.replaceStartEnd newStart newEnd h).startInclusive = newStart.str

@[simp]

theorem String.Slice.endExclusive_replaceStartEnd {s : Slice} {newStart newEnd : s.Pos} {h : newStart.offset ≤ newEnd.offset} : (s.replaceStartEnd newStart newEnd h).endExclusive = newEnd.str

def String.Slice.replaceStartEnd! (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.

@[simp]

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

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

@[simp]

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

@[simp]

theorem String.Slice.rawEndPos_replaceEnd {s : Slice} {pos : s.Pos} : (s.replaceEnd pos).rawEndPos = pos.offset

@[simp]

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

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

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

@[extern lean_string_utf8_get_fast]

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

Equations

• s.decodeChar byteIdx h = s.bytes.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.bytes.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.bytes.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 panicks 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!" 1149 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.ValidPos.toSlice {s : String} (pos : s.ValidPos) : 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.ValidPos.offset_toSlice {s : String} {pos : s.ValidPos} : pos.toSlice.offset = pos.offset

@[inline]

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

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

Equations

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

@[simp]

theorem String.Slice.Pos.offset_ofSlice {s : String} {pos : s.toSlice.Pos} : pos.ofSlice.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.endValidPos.toSlice

@[simp]

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

@[simp]

theorem String.ValidPos.ofSlice_toSlice {s : String} (pos : s.ValidPos) : pos.toSlice.ofSlice = pos

@[simp]

theorem String.Slice.Pos.toSlice_ofSlice {s : String} (pos : s.toSlice.Pos) : pos.ofSlice.toSlice = pos

@[simp]

theorem String.Slice.Pos.toSlice_comp_ofSlice {s : String} : ValidPos.toSlice ∘ ofSlice = id

@[simp]

theorem String.ValidPos.ofSlice_comp_toSlice {s : String} : Slice.Pos.ofSlice ∘ toSlice = id

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

theorem String.Slice.Pos.ofSlice_inj {s : String} {p q : s.toSlice.Pos} : p.ofSlice = q.ofSlice ↔ p = q

@[simp]

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

@[simp]

theorem String.Slice.Pos.ofSlice_le {s : String} {p q : s.toSlice.Pos} : p.ofSlice ≤ q.ofSlice ↔ p ≤ q

@[simp]

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

@[simp]

theorem String.Slice.Pos.ofSlice_lt {s : String} {p q : s.toSlice.Pos} : p.ofSlice < q.ofSlice ↔ p < q

@[inline]

def String.ValidPos.get {s : String} (pos : s.ValidPos) (h : pos ≠ s.endValidPos) : 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.ValidPos.get? {s : String} (pos : s.ValidPos) : 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.ValidPos.get! {s : String} (pos : s.ValidPos) : 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.ValidPos.byte {s : String} (pos : s.ValidPos) (h : pos ≠ s.endValidPos) : UInt8

Returns the byte at the position pos of a string.

Equations

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

theorem String.ValidPos.isUTF8FirstByte_byte {s : String} {pos : s.ValidPos} {h : pos ≠ s.endValidPos} : (pos.byte h).IsUTF8FirstByte

@[simp]

theorem String.startValidPos_eq_endValidPos_iff {b : String} : b.startValidPos = b.endValidPos ↔ b = ""

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

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

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

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

theorem String.get_startValidPos {b : String} (h : b.startValidPos ≠ b.endValidPos) : b.startValidPos.get h = b.toList.head ⋯

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

theorem String.Slice.copy_eq_copy_replaceEnd {s : Slice} {pos : s.Pos} : s.copy = (s.replaceEnd pos).copy ++ (s.replaceStart pos).copy

@[inline]

def String.ValidPos.ofCopy {s : Slice} (pos : s.copy.ValidPos) : 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.ValidPos.offset_ofCopy {s : Slice} {pos : s.copy.ValidPos} : pos.ofCopy.offset = pos.offset

@[inline]

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

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

Equations

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

@[simp]

theorem String.Slice.Pos.offset_toCopy {s : Slice} {pos : s.Pos} : pos.toCopy.offset = pos.offset

@[simp]

theorem String.Slice.Pos.ofCopy_toCopy {s : Slice} {pos : s.Pos} : pos.toCopy.ofCopy = pos

@[simp]

theorem String.ValidPos.toCopy_ofCopy {s : Slice} {pos : s.copy.ValidPos} : pos.ofCopy.toCopy = pos

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

@[simp]

theorem String.Slice.startValidPos_copy {s : Slice} : s.copy.startValidPos = s.startPos.toCopy

@[simp]

theorem String.Slice.endValidPos_copy {s : Slice} : s.copy.endValidPos = s.endPos.toCopy

theorem String.Slice.Pos.get_toCopy {s : Slice} {pos : s.Pos} (h : pos.toCopy ≠ s.copy.endValidPos) : pos.toCopy.get h = pos.get ⋯

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

theorem String.Slice.Pos.byte_toCopy {s : Slice} {pos : s.Pos} (h : pos.toCopy ≠ s.copy.endValidPos) : pos.toCopy.byte h = pos.byte ⋯

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

@[inline]

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

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

Equations

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

@[simp]

theorem String.Slice.Pos.offset_ofReplaceStart {s : Slice} {p₀ : s.Pos} {pos : (s.replaceStart p₀).Pos} : (ofReplaceStart pos).offset = pos.offset.offsetBy p₀.offset

@[inline]

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

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

Equations

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

@[simp]

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

@[simp]

theorem String.Slice.Pos.ofReplaceStart_startPos {s : Slice} {pos : s.Pos} : ofReplaceStart (s.replaceStart pos).startPos = pos

@[simp]

theorem String.Slice.Pos.ofReplaceStart_endPos {s : Slice} {pos : s.Pos} : ofReplaceStart (s.replaceStart pos).endPos = s.endPos

theorem String.Slice.Pos.ofReplaceStart_inj {s : Slice} {p₀ : s.Pos} {pos pos' : (s.replaceStart p₀).Pos} : ofReplaceStart pos = ofReplaceStart pos' ↔ pos = pos'

theorem String.Slice.Pos.get_eq_get_ofReplaceStart {s : Slice} {p₀ : s.Pos} {pos : (s.replaceStart p₀).Pos} {h : pos ≠ (s.replaceStart p₀).endPos} : pos.get h = (ofReplaceStart pos).get ⋯

@[inline]

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

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

Equations

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

@[simp]

theorem String.Slice.Pos.offset_ofReplaceEnd {s : Slice} {p₀ : s.Pos} {pos : (s.replaceEnd p₀).Pos} : (ofReplaceEnd pos).offset = pos.offset

@[inline]

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

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

Equations

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

@[simp]

theorem String.Slice.Pos.offset_toReplaceEnd {s : Slice} {p₀ pos : s.Pos} {h : pos ≤ p₀} : (p₀.toReplaceEnd 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.ValidPos.utf8ByteSize_byte {s : String} {pos : s.ValidPos} {h : pos ≠ s.endValidPos} : (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!" 1487 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_replaceEnd_append_get {s : Slice} {pos : s.Pos} (h : pos ≠ s.endPos) : s.copy = (s.replaceEnd pos).copy ++ singleton (pos.get h) ++ (s.replaceStart (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!" 1569 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.ValidPos.next {s : String} (pos : s.ValidPos) (h : pos ≠ s.endValidPos) : s.ValidPos

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 = (inline (pos.toSlice.next ⋯)).ofSlice

@[inline]

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

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.Slice.Pos.ofSlice pos.toSlice.next?

@[inline]

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

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! = pos.toSlice.next!.ofSlice

@[inline]

def String.ValidPos.prev {s : String} (pos : s.ValidPos) (h : pos ≠ s.startValidPos) : s.ValidPos

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 = (pos.toSlice.prev ⋯).ofSlice

@[inline]

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

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

Equations

• pos.prev? = Option.map String.Slice.Pos.ofSlice pos.toSlice.prev?

@[inline]

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

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

Equations

• pos.prev! = pos.toSlice.prev!.ofSlice

@[inline]

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

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

Equations

• s.pos off h = (s.toSlice.pos off ⋯).ofSlice

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

• s.pos! off = (s.toSlice.pos! off).ofSlice

@[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.ValidPos.cast {s t : String} (pos : s.ValidPos) (h : s = t) : t.ValidPos

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.ValidPos.offset_cast {s t : String} {pos : s.ValidPos} {h : s = t} : (pos.cast h).offset = pos.offset

@[simp]

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

theorem String.ValidPos.toCopy_toSlice_eq_cast {s : String} (p : s.ValidPos) : p.toSlice.toCopy = 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.ValidPos.prev_ne_endValidPos {s : String} {p : s.ValidPos} {h : p ≠ s.startValidPos} : p.prev h ≠ s.endValidPos

theorem String.ValidPos.toSlice_prev {s : String} {p : s.ValidPos} {h : p ≠ s.startValidPos} : (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.ValidPos.prev_lt {s : String} {p : s.ValidPos} {h : p ≠ s.startValidPos} : p.prev h < p

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.ValidPos.nextn {s : String} (p : s.ValidPos) (n : Nat) : s.ValidPos

Advances the position p n times.

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

Equations

• p.nextn n = (p.toSlice.nextn n).ofSlice

@[inline]

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

Iterates p.prev n times.

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

Equations

• p.prevn n = (p.toSlice.prevn n).ofSlice

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.ValidPos.get, combined with String.pos or another means of obtaining a String.ValidPos.

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.ValidPos.get, combined with String.pos? or another means of obtaining a String.ValidPos.

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.ValidPos.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.ValidPos.get, combined with String.pos! or another means of obtaining a String.ValidPos.

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.ValidPos.get_toSlice {s : String} {p : s.ValidPos} {h : p.toSlice ≠ s.toSlice.endPos} : p.toSlice.get h = p.get ⋯

theorem String.ValidPos.get_eq_get_toSlice {s : String} {p : s.ValidPos} {h : p ≠ s.endValidPos} : p.get h = p.toSlice.get ⋯

@[simp]

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

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

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

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

@[simp]

theorem String.ValidPos.lt_next {s : String} (p : s.ValidPos) {h : p ≠ s.endValidPos} : p < p.next h

theorem String.ValidPos.ne_startPos_of_lt {s : String} {p q : s.ValidPos} : p < q → q ≠ s.startValidPos

theorem String.ValidPos.next_ne_startValidPos {s : String} {p : s.ValidPos} {h : p ≠ s.endValidPos} : p.next h ≠ s.startValidPos

@[simp]

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

@[inline]

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

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

Equations

• s.replaceEnd p = s.toSlice.replaceEnd p.toSlice

@[simp]

theorem String.str_replaceEnd {s : String} {p : s.ValidPos} : (s.replaceEnd p).str = s

@[simp]

theorem String.startInclusive_replaceEnd {s : String} {p : s.ValidPos} : (s.replaceEnd p).startInclusive = s.startValidPos

@[simp]

theorem String.endExclusive_replaceEnd {s : String} {p : s.ValidPos} : (s.replaceEnd p).endExclusive = p

@[simp]

theorem String.rawEndPos_replaceEnd {s : String} {p : s.ValidPos} : (s.replaceEnd p).rawEndPos = p.offset

theorem String.Pos.Raw.isValidForSlice_stringReplaceEnd {s : String} {p : s.ValidPos} {q : Raw} : IsValidForSlice (s.replaceEnd p) q ↔ q ≤ p.offset ∧ IsValid s q

@[inline]

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

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

Equations

• s.replaceStart p = s.toSlice.replaceStart p.toSlice

@[simp]

theorem String.str_replaceStart {s : String} {p : s.ValidPos} : (s.replaceStart p).str = s

@[simp]

theorem String.startInclusive_replaceStart {s : String} {p : s.ValidPos} : (s.replaceStart p).startInclusive = p

@[simp]

theorem String.endExclusive_replaceStart {s : String} {p : s.ValidPos} : (s.replaceStart p).endExclusive = s.endValidPos

@[simp]

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

@[simp]

theorem String.utf8ByteSize_replaceStart {s : String} {p : s.ValidPos} : (s.replaceStart p).utf8ByteSize = s.utf8ByteSize - p.offset.byteIdx

@[simp]

theorem String.utf8ByteSize_replaceEnd {s : String} {p : s.ValidPos} : (s.replaceEnd p).utf8ByteSize = p.offset.byteIdx

theorem String.Pos.Raw.isValidForSlice_stringReplaceStart {s : String} {p : s.ValidPos} {q : Raw} : IsValidForSlice (s.replaceStart p) q ↔ IsValid s (q.offsetBy p.offset)

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

Equations

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

theorem String.ValidPos.utf8Encode_get_eq_extract {s : String} (pos : s.ValidPos) (h : pos ≠ s.endValidPos) : [pos.get h].utf8Encode = s.bytes.extract pos.offset.byteIdx (pos.offset.byteIdx + (pos.get h).utf8Size)

theorem String.ValidPos.eq_copy_replaceEnd_append_get {s : String} {pos : s.ValidPos} (h : pos ≠ s.endValidPos) : s = (s.replaceEnd pos).copy ++ singleton (pos.get h) ++ (s.replaceStart (pos.next h)).copy

@[inline]

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

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

Equations

• String.ValidPos.ofReplaceStart pos = { offset := pos.offset.offsetBy p₀.offset, isValid := ⋯ }

@[simp]

theorem String.ValidPos.offset_ofReplaceStart {s : String} {p₀ : s.ValidPos} {pos : (s.replaceStart p₀).Pos} : (ofReplaceStart pos).offset = pos.offset.offsetBy p₀.offset

@[inline]

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

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

Equations

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

@[simp]

theorem String.ValidPos.offset_toReplaceStart {s : String} {p₀ pos : s.ValidPos} {h : p₀ ≤ pos} : (p₀.toReplaceStart pos h).offset = pos.offset.unoffsetBy p₀.offset

@[simp]

theorem String.ValidPos.ofReplaceStart_startPos {s : String} {pos : s.ValidPos} : ofReplaceStart (s.replaceStart pos).startPos = pos

@[simp]

theorem String.ValidPos.ofReplaceStart_endPos {s : String} {pos : s.ValidPos} : ofReplaceStart (s.replaceStart pos).endPos = s.endValidPos

theorem String.ValidPos.ofReplaceStart_inj {s : String} {p₀ : s.ValidPos} {pos pos' : (s.replaceStart p₀).Pos} : ofReplaceStart pos = ofReplaceStart pos' ↔ pos = pos'

theorem String.ValidPos.get_eq_get_ofReplaceStart {s : String} {p₀ : s.ValidPos} {pos : (s.replaceStart p₀).Pos} {h : pos ≠ (s.replaceStart p₀).endPos} : pos.get h = (ofReplaceStart pos).get ⋯

@[inline]

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

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

Equations

• String.ValidPos.ofReplaceEnd pos = { offset := pos.offset, isValid := ⋯ }

@[simp]

theorem String.ValidPos.offset_ofReplaceEnd {s : String} {p₀ : s.ValidPos} {pos : (s.replaceEnd p₀).Pos} : (ofReplaceEnd pos).offset = pos.offset

@[inline]

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

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

Equations

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

@[simp]

theorem String.ValidPos.offset_toReplaceEnd {s : String} {p₀ pos : s.ValidPos} {h : pos ≤ p₀} : (p₀.toReplaceEnd pos h).offset = pos.offset

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

theorem String.ValidPos.le_nextn {s : String} {p : s.ValidPos} {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.ValidPos.prevn_le {s : String} {p : s.ValidPos} {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.ValidPos.next or one of its variants like String.ValidPos.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.ValidPos.prev or one of its variants like String.ValidPos.prev?, combined with String.pos or another means of obtaining a String.ValidPos.

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✝

@[inline]

def String.front (s : String) : Char

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

Examples:

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

Equations

• s.front = String.Pos.Raw.get s 0

@[export lean_string_front]

def String.Internal.frontImpl (s : String) : Char

Equations

• String.Internal.frontImpl s = s.front

theorem String.front_eq_get {s : String} : s.front = Pos.Raw.get s 0

@[inline]

def String.back (s : String) : Char

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

Examples:

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

Equations

• s.back = String.Pos.Raw.get s (String.Pos.Raw.prev s s.rawEndPos)

theorem String.back_eq_get_prev_rawEndPos {s : String} : s.back = Pos.Raw.get s (Pos.Raw.prev s s.rawEndPos)

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

theorem String.back_eq_get_prev_endPos {s : String} : s.back = Pos.Raw.get s (Pos.Raw.prev s s.rawEndPos)

@[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.ValidPos.get, combined with String.pos or another means of obtaining a String.ValidPos.

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.ValidPos.next, combined with String.pos or another means of obtaining a String.ValidPos.

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

@[irreducible]

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

Equations

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

@[inline]

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

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

Examples:

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

Equations

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

@[export lean_string_posof]

def String.Internal.posOfImpl (s : String) (c : Char) : Pos.Raw

Equations

• String.Internal.posOfImpl s c = s.posOf c

@[irreducible]

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

Equations

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

@[inline]

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

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

Examples:

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

Equations

• s.revPosOf c = s.revPosOfAux c s.rawEndPos

@[irreducible]

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

Equations

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

@[inline]

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

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

Examples:

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

Equations

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

@[irreducible]

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

Equations

• s.revFindAux p pos = if h : pos = 0 then none else have this := ⋯; have pos := String.Pos.Raw.prev s pos; if p (String.Pos.Raw.get s pos) = true then some pos else s.revFindAux p pos

@[inline]

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

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

Examples:

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

Equations

• s.revFind p = s.revFindAux p s.rawEndPos

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.ValidPos.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✝

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

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

Equations

• x✝².extract x✝¹ x✝ = String.Pos.Raw.extract x✝² x✝¹ x✝

@[irreducible, specialize #[]]

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

Equations

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

@[inline]

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

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

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

Examples:

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

Equations

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

@[inline, deprecated String.splitToList (since := "2025-10-17")]

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

Equations

• s.split p = s.splitToList p

@[irreducible]

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

Auxiliary for splitOn. Preconditions:

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

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

Equations

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

@[inline]

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

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

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

Examples:

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

Equations

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

@[irreducible]

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

Equations

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

@[inline]

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

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

@[export lean_string_offsetofpos]

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

Equations

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

@[irreducible, specialize #[]]

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

Equations

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

@[inline]

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

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

Examples:

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

Equations

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

@[export lean_string_foldl]

def String.Internal.foldlImpl (f : String → Char → String) (init s : String) : String

Equations

• String.Internal.foldlImpl f init s = String.foldl f init s

@[irreducible, specialize #[]]

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

Equations

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

@[inline]

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

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

Examples:

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

Equations

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

@[irreducible, specialize #[]]

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

Equations

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

@[inline]

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

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

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

Examples:

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

Equations

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

@[export lean_string_any]

def String.Internal.anyImpl (s : String) (p : Char → Bool) : Bool

Equations

• String.Internal.anyImpl s p = s.any p

@[inline]

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

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

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

Examples:

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

Equations

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

@[inline]

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

Checks whether a string contains the specified character.

Examples:

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

Equations

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

@[export lean_string_contains]

def String.Internal.containsImpl (s : String) (c : Char) : Bool

Equations

• String.Internal.containsImpl s c = s.contains c

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

@[inline]

def String.isNat (s : String) : Bool

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

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

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

Examples:

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

Equations

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

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

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

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

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

Examples:

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

Equations

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

def String.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

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

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

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

Examples:

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

Equations

• p.isPrefixOf s = String.Pos.Raw.substrEq p 0 s 0 p.rawEndPos.byteIdx

@[export lean_string_isprefixof]

def String.Internal.isPrefixOfImpl (p s : String) : Bool

Equations

• String.Internal.isPrefixOfImpl p s = p.isPrefixOf s

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

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

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

Equations

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

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

@[simp]

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