@[simp]

theorem List.utf8Encode_nil : [].utf8Encode = ByteArray.empty

theorem List.utf8Encode_singleton {c : Char} : [c].utf8Encode = (String.utf8EncodeChar c).toByteArray

@[simp]

theorem List.utf8Encode_append {l l' : List Char} : (l ++ l').utf8Encode = l.utf8Encode ++ l'.utf8Encode

theorem List.utf8Encode_cons {c : Char} {l : List Char} : (c :: l).utf8Encode = [c].utf8Encode ++ l.utf8Encode

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

@[simp]

theorem String.utf8EncodeChar_ne_nil {c : Char} : utf8EncodeChar c ≠ []

@[simp]

theorem List.utf8Encode_eq_empty {l : List Char} : l.utf8Encode = ByteArray.empty ↔ l = []

theorem ByteArray.isValidUTF8_utf8Encode {l : List Char} : l.utf8Encode.IsValidUTF8

@[simp]

theorem ByteArray.isValidUTF8_empty : empty.IsValidUTF8

theorem Char.isValidUTF8_toByteArray_utf8EncodeChar {c : Char} : (String.utf8EncodeChar c).toByteArray.IsValidUTF8

theorem ByteArray.IsValidUTF8.append {b b' : ByteArray} (h : b.IsValidUTF8) (h' : b'.IsValidUTF8) : (b ++ b').IsValidUTF8

@[simp]

theorem Char.toUInt8_val {c : Char} : c.val.toUInt8 = c.toUInt8

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) (h : a.IsValidUTF8) : String

Decodes an array of bytes that encode a string as UTF-8 into the corresponding string.

Equations

• String.fromUTF8 a h = { bytes := a, isValidUTF8 := h }

@[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!" 243 46 "invalid UTF-8 string"

@[extern lean_string_to_utf8]

def String.toUTF8 (a : String) : ByteArray

Encodes a string in UTF-8 as an array of bytes.

Equations

• a.toUTF8 = a.bytes

@[simp]

theorem String.toUTF8_eq_bytes {s : String} : s.toUTF8 = s.bytes

@[simp]

theorem String.bytes_empty : "".bytes = ByteArray.empty

@[extern lean_string_append]

def String.append (s : String) (t : String) : String

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

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

Examples:

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

Equations

• s.append t = { bytes := s.bytes ++ t.bytes, isValidUTF8 := ⋯ }

instance instAppendString : Append String

Equations

• instAppendString = { append := fun (s t : String) => s.append t }

@[simp]

theorem String.bytes_append {s t : String} : (s ++ t).bytes = s.bytes ++ t.bytes

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

@[simp]

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

@[simp]

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

@[simp]

theorem List.bytes_asString {l : List Char} : l.asString.bytes = l.utf8Encode

@[simp]

theorem List.asString_nil : [].asString = ""

@[simp]

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

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.data (b : String) : List Char

Equations

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

@[simp]

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

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

@[simp]

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

@[simp]

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

theorem String.exists_eq_asString (s : String) : ∃ (l : List Char), s = l.asString

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 List.data_asString {l : List Char} : l.asString.data = l

@[simp]

theorem String.asString_data {b : String} : b.data.asString = b

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem String.utf8ByteSize_empty : "".utf8ByteSize = 0

@[simp]

theorem String.utf8ByteSize_append {s t : String} : (s ++ t).utf8ByteSize = s.utf8ByteSize + t.utf8ByteSize

@[simp]

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

@[simp]

theorem String.bytes_push {s : String} {c : Char} : (s.push c).bytes = s.bytes ++ [c].utf8Encode

instance String.instHSubRaw : HSub Pos.Raw String Pos.Raw

Equations

• String.instHSubRaw = { hSub := fun (p : String.Pos.Raw) (s : String) => { byteIdx := p.byteIdx - s.utf8ByteSize } }

instance String.instHSubRawChar : HSub Pos.Raw Char Pos.Raw

Equations

• String.instHSubRawChar = { hSub := fun (p : String.Pos.Raw) (c : Char) => { byteIdx := p.byteIdx - c.utf8Size } }

@[export lean_string_pos_sub]

def String.Pos.Internal.subImpl : Raw → Raw → Raw

Equations

• String.Pos.Internal.subImpl p₁ p₂ = { byteIdx := p₁.byteIdx - p₂.byteIdx }

instance String.instHAddRawChar : HAdd Pos.Raw Char Pos.Raw

Equations

• String.instHAddRawChar = { hAdd := fun (p : String.Pos.Raw) (c : Char) => { byteIdx := p.byteIdx + c.utf8Size } }

instance String.instHAddCharRaw : HAdd Char Pos.Raw Pos.Raw

Equations

• String.instHAddCharRaw = { hAdd := fun (c : Char) (p : String.Pos.Raw) => { byteIdx := c.utf8Size + p.byteIdx } }

instance String.instHAddRaw : HAdd String Pos.Raw Pos.Raw

Equations

• String.instHAddRaw = { hAdd := fun (s : String) (p : String.Pos.Raw) => { byteIdx := s.utf8ByteSize + p.byteIdx } }

instance String.instHAddRaw_1 : HAdd Pos.Raw String Pos.Raw

Equations

• String.instHAddRaw_1 = { hAdd := fun (p : String.Pos.Raw) (s : String) => { byteIdx := p.byteIdx + s.utf8ByteSize } }

instance String.instLERaw : LE Pos.Raw

Equations

• String.instLERaw = { le := fun (p₁ p₂ : String.Pos.Raw) => p₁.byteIdx ≤ p₂.byteIdx }

instance String.instLTRaw : LT Pos.Raw

Equations

• String.instLTRaw = { lt := fun (p₁ p₂ : String.Pos.Raw) => p₁.byteIdx < p₂.byteIdx }

instance String.instDecidableLeRaw (p₁ p₂ : Pos.Raw) : Decidable (p₁ ≤ p₂)

Equations

• String.instDecidableLeRaw p₁ p₂ = inferInstanceAs (Decidable (p₁.byteIdx ≤ p₂.byteIdx))

instance String.instDecidableLtRaw (p₁ p₂ : Pos.Raw) : Decidable (p₁ < p₂)

Equations

• String.instDecidableLtRaw p₁ p₂ = inferInstanceAs (Decidable (p₁.byteIdx < p₂.byteIdx))

instance String.instMinRaw : Min Pos.Raw

Equations

• String.instMinRaw = minOfLe

instance String.instMaxRaw : Max Pos.Raw

Equations

• String.instMaxRaw = maxOfLe

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

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

@[simp]

theorem String.byteIdx_endPos {s : String} : s.endPos.byteIdx = s.utf8ByteSize

@[simp]

theorem String.utf8ByteSize_ofByteArray {b : ByteArray} {h : b.IsValidUTF8} : { bytes := b, isValidUTF8 := h }.utf8ByteSize = b.size

theorem String.Pos.Raw.ext_iff {x y : Raw} : x = y ↔ x.byteIdx = y.byteIdx

theorem String.Pos.Raw.ext {x y : Raw} (byteIdx : x.byteIdx = y.byteIdx) : x = y

instance String.instLT : LT String

Equations

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

@[extern lean_string_dec_lt]

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

Equations

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

@[reducible]

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₁)

@[inline]

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 = s.data

structure String.Pos.Raw.IsValid (s : String) (off : Raw) : Prop

Predicate for validity of positions inside a String.

There are multiple equivalent definitions for validity.

We say that a position is valid if the string obtained by taking all of the bytes up to, but excluding, the given position, is valid UTF-8; see Pos.isValid_iff_isValidUTF8_extract_zero.

Similarly, a position is valid if the string obtained by taking all of the bytes starting at the given position is valid UTF-8; see Pos.isValid_iff_isValidUTF8_extract_utf8ByteSize.

An equivalent condition is that the position is the length of the UTF-8 encoding of some prefix of the characters of the string; see Pos.isValid_iff_exists_append and Pos.isValid_iff_exists_take_data.

Another equivalent condition that can be checked efficiently is that the position is either the end position or strictly smaller than the end position and the byte at the position satisfies UInt8.IsUTF8FirstByte; see Pos.isValid_iff_isUTF8FirstByte.

Examples:

• String.Pos.IsValid "abc" ⟨0⟩
• String.Pos.IsValid "abc" ⟨1⟩
• String.Pos.IsValid "abc" ⟨3⟩
• ¬ String.Pos.IsValid "abc" ⟨4⟩
• String.Pos.IsValid "𝒫(A)" ⟨0⟩
• ¬ String.Pos.IsValid "𝒫(A)" ⟨1⟩
• ¬ String.Pos.IsValid "𝒫(A)" ⟨2⟩
• ¬ String.Pos.IsValid "𝒫(A)" ⟨3⟩
• String.Pos.IsValid "𝒫(A)" ⟨4⟩

• le_endPos : off ≤ s.endPos
• isValidUTF8_extract_zero : (s.bytes.extract 0 off.byteIdx).IsValidUTF8

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 ∧ (m₁ ++ m₂).asString = 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₁.endPos

@[simp]

theorem String.Pos.Raw.byteIdx_zero : byteIdx 0 = 0

@[simp]

theorem String.Pos.Raw.isValid_zero {s : String} : IsValid s 0

@[simp]

theorem String.Pos.Raw.isValid_endPos {s : String} : IsValid s s.endPos

@[simp]

theorem String.Pos.Raw.isValid_empty_iff {p : Raw} : IsValid "" p ↔ p = 0

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

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

@[simp]

theorem String.bytes_singleton {c : Char} : (singleton c).bytes = [c].utf8Encode

theorem String.singleton_eq_asString {c : Char} : singleton c = [c].asString

@[simp]

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

@[simp]

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

@[inline]

def String.Pos.Raw.byteDistance (lo hi : Raw) : Nat

Returns the size of the byte slice delineated by the positions lo and hi.

Equations

• lo.byteDistance hi = hi.byteIdx - lo.byteIdx

theorem String.Pos.Raw.byteDistance_eq {lo hi : Raw} : lo.byteDistance hi = hi.byteIdx - lo.byteIdx

@[simp]

theorem String.Pos.Raw.byteIdx_sub_char {p : Raw} {c : Char} : (p - c).byteIdx = p.byteIdx - c.utf8Size

@[simp]

theorem String.Pos.Raw.byteIdx_sub_string {p : Raw} {s : String} : (p - s).byteIdx = p.byteIdx - s.utf8ByteSize

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem String.Pos.Raw.isValid_append {s t : String} {p : Raw} : IsValid (s ++ t) p ↔ IsValid s p ∨ s.endPos ≤ 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

@[simp]

theorem String.append_singleton {s : String} {c : Char} : s ++ singleton c = s.push c

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

@[simp]

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

theorem String.endPos_push {s : String} {c : Char} : (s.push c).endPos = s.endPos + 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

@[extern lean_string_get_byte_fast]

def String.getUTF8Byte (s : String) (p : Pos.Raw) (h : p < s.endPos) : UInt8

Accesses the indicated byte in the UTF-8 encoding of a string.

At runtime, this function is implemented by efficient, constant-time code.

Equations

• s.getUTF8Byte p h = s.bytes[p.byteIdx]

@[reducible, inline, extern lean_string_get_byte_fast, deprecated String.getUTF8Byte (since := "2025-10-01")]

abbrev String.getUtf8Byte (s : String) (p : Pos.Raw) (h : p < s.endPos) : UInt8

Equations

• s.getUtf8Byte p h = s.getUTF8Byte p h

@[simp]

theorem String.endPos_empty : "".endPos = 0

theorem String.Pos.Raw.isValid_iff_isUTF8FirstByte {s : String} {p : Raw} : IsValid s p ↔ p = s.endPos ∨ ∃ (h : p < s.endPos), (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.endPos and p lies on a UTF-8 character boundary. At runtime, this operation takes constant time.

Examples:

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

Equations

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

@[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.endPos ∨ (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.endPos} : (b.getUTF8Byte 0 h).IsUTF8FirstByte

theorem String.Pos.Raw.le_trans {a b c : Raw} : a ≤ b → b ≤ c → a ≤ c

theorem String.Pos.Raw.lt_of_lt_of_le {a b c : Raw} : a < b → b ≤ c → a < c

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

theorem String.Pos.Raw.isValid_iff_isValidUTF8_extract_zero {s : String} {p : Raw} : IsValid s p ↔ p ≤ s.endPos ∧ (s.bytes.extract 0 p.byteIdx).IsValidUTF8

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

structure String.ValidPos (s : String) : Type

A ValidPos s is a byte offset in s together with a proof that this position is at a UTF-8 character boundary.

• offset : Pos.Raw

  The underlying byte offset of the ValidPos.

• isValid : Pos.Raw.IsValid s self.offset

  The proof that offset is valid for the string s.

theorem String.ValidPos.ext_iff {s : String} {x y : s.ValidPos} : x = y ↔ x.offset = y.offset

theorem String.ValidPos.ext {s : String} {x y : s.ValidPos} (offset : x.offset = y.offset) : x = y

def String.instDecidableEqValidPos.decEq {s✝ : String} (x✝ x✝¹ : s✝.ValidPos) : Decidable (x✝ = x✝¹)

Equations

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

instance String.instDecidableEqValidPos {s✝ : String} : DecidableEq s✝.ValidPos

Equations

• String.instDecidableEqValidPos = String.instDecidableEqValidPos.decEq

@[inline]

def String.startValidPos (s : String) : s.ValidPos

The start position of s, as an s.ValidPos.

Equations

• s.startValidPos = { offset := 0, isValid := ⋯ }

instance String.instInhabitedValidPos {s : String} : Inhabited s.ValidPos

Equations

• String.instInhabitedValidPos = { default := s.startValidPos }

@[simp]

theorem String.offset_startValidPos {s : String} : s.startValidPos.offset = 0

@[inline]

def String.endValidPos (s : String) : s.ValidPos

The past-the-end position of s, as an s.ValidPos.

Equations

• s.endValidPos = { offset := s.endPos, isValid := ⋯ }

instance String.instLEValidPos {s : String} : LE s.ValidPos

Equations

• String.instLEValidPos = { le := fun (l r : s.ValidPos) => l.offset ≤ r.offset }

instance String.instLTValidPos {s : String} : LT s.ValidPos

Equations

• String.instLTValidPos = { lt := fun (l r : s.ValidPos) => l.offset < r.offset }

theorem String.ValidPos.le_iff {s : String} {l r : s.ValidPos} : l ≤ r ↔ l.offset ≤ r.offset

theorem String.ValidPos.lt_iff {s : String} {l r : s.ValidPos} : l < r ↔ l.offset < r.offset

instance String.instDecidableLeValidPos {s : String} (l r : s.ValidPos) : Decidable (l ≤ r)

Equations

• String.instDecidableLeValidPos l r = decidable_of_iff' (l.offset ≤ r.offset) ⋯

instance String.instDecidableLtValidPos {s : String} (l r : s.ValidPos) : Decidable (l < r)

Equations

• String.instDecidableLtValidPos l r = decidable_of_iff' (l.offset < r.offset) ⋯

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

structure String.Slice : Type

A region or slice of some underlying string.

A slice consists of a string together with the start and end byte positions of a region of interest. Actually extracting a substring requires copying and memory allocation, while many slices of the same underlying string may exist with very little overhead. While this could be achieved by tracking the bounds by hand, the slice API is much more convenient.

String.Slice bundles proofs to ensure that the start and end positions always delineate a valid string. For this reason, it should be preferred over Substring.

• str : String

  The underlying strings.

• startInclusive : self.str.ValidPos

  The byte position of the start of the string slice.

• endExclusive : self.str.ValidPos

  The byte position of the end of the string slice.

• startInclusive_le_endExclusive : self.startInclusive ≤ self.endExclusive

  The slice is not degenerate (but it may be empty).

instance String.instInhabitedSlice : Inhabited Slice

Equations

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

@[inline]

def String.toSlice (s : String) : Slice

Returns a slice that contains the entire string.

Equations

• s.toSlice = { str := s, startInclusive := s.startValidPos, endExclusive := s.endValidPos, startInclusive_le_endExclusive := ⋯ }

def String.Slice.utf8ByteSize (s : Slice) : Nat

The number of bytes of the UTF-8 encoding of the string slice.

Equations

• s.utf8ByteSize = s.startInclusive.offset.byteDistance s.endExclusive.offset

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

instance String.instHAddRawSlice : HAdd Pos.Raw Slice Pos.Raw

Equations

• String.instHAddRawSlice = { hAdd := fun (p : String.Pos.Raw) (s : String.Slice) => { byteIdx := p.byteIdx + s.utf8ByteSize } }

instance String.instHAddSliceRaw : HAdd Slice Pos.Raw Pos.Raw

Equations

• String.instHAddSliceRaw = { hAdd := fun (s : String.Slice) (p : String.Pos.Raw) => { byteIdx := s.utf8ByteSize + p.byteIdx } }

instance String.instHSubRawSlice : HSub Pos.Raw Slice Pos.Raw

Equations

• String.instHSubRawSlice = { hSub := fun (p : String.Pos.Raw) (s : String.Slice) => { byteIdx := p.byteIdx - s.utf8ByteSize } }

@[simp]

theorem String.Pos.Raw.byteIdx_add_slide {p : Raw} {s : Slice} : (p + s).byteIdx = p.byteIdx + s.utf8ByteSize

@[simp]

theorem String.Pos.Raw.byteIdx_slice_add {s : Slice} {p : Raw} : (s + p).byteIdx = s.utf8ByteSize + p.byteIdx

@[simp]

theorem String.Pos.Raw.byteIdx_sub_slice {p : Raw} {s : Slice} : (p - s).byteIdx = p.byteIdx - s.utf8ByteSize

def String.Slice.rawEndPos (s : Slice) : Pos.Raw

The end position of a slice, as a Pos.Raw.

Equations

• s.rawEndPos = { byteIdx := s.utf8ByteSize }

@[simp]

theorem String.Slice.byteIdx_rawEndPos {s : Slice} : s.rawEndPos.byteIdx = s.utf8ByteSize

@[inline]

def String.Pos.Raw.offsetBy (p offset : Raw) : Raw

Offsets p by offset on the left. This is not an HAdd instance because it should be a relatively rare operation, so we use a name to make accidental use less likely. To offset a position by the size of a character character c or string s, you can use c + p resp. s + p.

This should be seen as an operation that converts relative positions into absolute positions.

See also Pos.Raw.increaseBy, which is an "advancing" operation.

Equations

• p.offsetBy offset = { byteIdx := offset.byteIdx + p.byteIdx }

@[simp]

theorem String.Pos.Raw.byteIdx_offsetBy {p offset : Raw} : (p.offsetBy offset).byteIdx = offset.byteIdx + p.byteIdx

@[inline]

def String.Pos.Raw.unoffsetBy (p offset : Raw) : Raw

Decreases p by offset. This is not an HSub instance because it should be a relatively rare operation, so we use a name to make accidental use less likely. To unoffset a position by the size of a character c or string s, you can use p - c resp. p - s.

This should be seen as an operation that converts absolute positions into relative positions.

See also Pos.Raw.decreaseBy, which is an "unadvancing" operation.

Equations

• p.unoffsetBy offset = { byteIdx := p.byteIdx - offset.byteIdx }

@[simp]

theorem String.Pos.Raw.byteIdx_unoffsetBy {p offset : Raw} : (p.unoffsetBy offset).byteIdx = p.byteIdx - offset.byteIdx

structure String.Pos.Raw.IsValidForSlice (s : Slice) (p : Raw) : Prop

Criterion for validity of positions in string slices.

• le_utf8ByteSize : p ≤ s.rawEndPos
• isValid_offsetBy : IsValid s.str (p.offsetBy s.startInclusive.offset)

@[inline]

def String.Slice.getUTF8Byte (s : Slice) (p : Pos.Raw) (h : p < s.rawEndPos) : UInt8

Accesses the indicated byte in the UTF-8 encoding of a string slice.

At runtime, this function is implemented by efficient, constant-time code.

Equations

• s.getUTF8Byte p h = s.str.getUTF8Byte (p.offsetBy s.startInclusive.offset) ⋯

def String.Slice.getUTF8Byte! (s : Slice) (p : Pos.Raw) : UInt8

Accesses the indicated byte in the UTF-8 encoding of the string slice, or panics if the position is out-of-bounds.

Equations

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

@[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.endPos_copy {s : Slice} : s.copy.endPos = s.rawEndPos

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.endPos} : 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

structure String.Slice.Pos (s : Slice) : Type

A Slice.Pos s is a byte offset in s together with a proof that this position is at a UTF-8 character boundary.

• offset : Pos.Raw

  The underlying byte offset of the Slice.Pos.

• isValidForSlice : Pos.Raw.IsValidForSlice s self.offset

  The proof that offset is valid for the string slice s.

theorem String.Slice.Pos.ext {s : Slice} {x y : s.Pos} (offset : x.offset = y.offset) : x = y

theorem String.Slice.Pos.ext_iff {s : Slice} {x y : s.Pos} : x = y ↔ x.offset = y.offset

def String.Slice.instDecidableEqPos.decEq {s✝ : Slice} (x✝ x✝¹ : s✝.Pos) : Decidable (x✝ = x✝¹)

Equations

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

instance String.Slice.instDecidableEqPos {s✝ : Slice} : DecidableEq s✝.Pos

Equations

• String.Slice.instDecidableEqPos = String.Slice.instDecidableEqPos.decEq

@[inline]

def String.Slice.startPos (s : Slice) : s.Pos

The start position of s, as an s.Pos.

Equations

• s.startPos = { offset := 0, isValidForSlice := ⋯ }

@[simp]

theorem String.ByteString.Slice.offset_startPos {s : Slice} : s.startPos.offset = 0

instance String.instInhabitedPos {s : Slice} : Inhabited s.Pos

Equations

• String.instInhabitedPos = { default := s.startPos }

@[simp]

theorem String.Slice.offset_startInclusive_add_self {s : Slice} : s.startInclusive.offset + s = s.endExclusive.offset

@[simp]

theorem String.Pos.Raw.offsetBy_endPos_left {p : Raw} {s : String} : s.endPos.offsetBy p = p + s

@[simp]

theorem String.Pos.Raw.offsetBy_endPos_right {p : Raw} {s : String} : p.offsetBy s.endPos = s + p

@[simp]

theorem String.Pos.Raw.offsetBy_sliceRawEndPos_left {p : Raw} {s : Slice} : s.rawEndPos.offsetBy p = p + s

@[simp]

theorem String.Pos.Raw.offsetBy_sliceRawEndPos_right {p : Raw} {s : Slice} : p.offsetBy s.rawEndPos = s + p

@[inline]

def String.Slice.endPos (s : Slice) : s.Pos

The past-the-end position of s, as an s.Pos.

Equations

• s.endPos = { offset := s.rawEndPos, isValidForSlice := ⋯ }

@[simp]

theorem String.ByteString.Slice.offset_endPos {s : Slice} : s.endPos.offset = s.rawEndPos

instance String.instLEPos {s : Slice} : LE s.Pos

Equations

• String.instLEPos = { le := fun (l r : s.Pos) => l.offset ≤ r.offset }

instance String.instLTPos {s : Slice} : LT s.Pos

Equations

• String.instLTPos = { lt := fun (l r : s.Pos) => l.offset < r.offset }

theorem String.Slice.Pos.le_iff {s : Slice} {l r : s.Pos} : l ≤ r ↔ l.offset ≤ r.offset

theorem String.Slice.Pos.lt_iff {s : Slice} {l r : s.Pos} : l < r ↔ l.offset < r.offset

instance String.instDecidableLePos {s : Slice} (l r : s.Pos) : Decidable (l ≤ r)

Equations

• String.instDecidableLePos l r = decidable_of_iff' (l.offset ≤ r.offset) ⋯

instance String.instDecidableLtPos {s : Slice} (l r : s.Pos) : Decidable (l < r)

Equations

• String.instDecidableLtPos l r = decidable_of_iff' (l.offset < r.offset) ⋯

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

@[inline]

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

Returns the byte at a position in a slice that is not the end position.

Equations

• pos.byte h = s.getUTF8Byte pos.offset ⋯

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.offsetBy_assoc {p q r : Raw} : (p.offsetBy q).offsetBy r = p.offsetBy (q.offsetBy r)

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]

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) ⋯

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!" 1603 29 "Cannot retrieve character at end position" else pos.get h

@[simp]

theorem String.startInclusive_toSlice {s : String} : s.toSlice.startInclusive = s.startValidPos

@[simp]

theorem String.endExclusive_toSlice {s : String} : s.toSlice.endExclusive = s.endValidPos

@[simp]

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

@[simp]

theorem String.offset_endValidPos {s : String} : s.endValidPos.offset = s.endPos

@[simp]

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

@[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.ofset_ofSlice {s : String} {pos : s.toSlice.Pos} : pos.ofSlice.offset = pos.offset

@[simp]

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

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

@[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.append_left_inj {s₁ s₂ : String} (t : String) : s₁ ++ t = s₂ ++ t ↔ s₁ = s₂

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

@[simp]

theorem String.utf8ByteSize_eq_zero_iff {s : String} : s.utf8ByteSize = 0 ↔ s = ""

@[simp]

theorem String.Pos.Raw.eq_zero_iff {p : Raw} : p = 0 ↔ p.byteIdx = 0

theorem String.endPos_eq_zero_iff {b : String} : b.endPos = 0 ↔ b = ""

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem List.length_asString {l : List Char} : l.asString.length = l.length

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

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

theorem String.get_startValidPos {b : String} (h : b.startValidPos ≠ b.endValidPos) : b.startValidPos.get h = b.data.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

theorem String.Pos.Raw.offsetBy_unoffsetBy_of_le {p q : Raw} (h : q ≤ p) : (p.unoffsetBy q).offsetBy q = p

@[simp]

theorem String.Pos.Raw.unoffsetBy_offsetBy {p q : Raw} : (p.offsetBy q).unoffsetBy q = p

@[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.Pos.Raw.offsetBy_zero_left {p : Raw} : offsetBy 0 p = p

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

@[inline]

def String.Pos.Raw.increaseBy (p : Raw) (n : Nat) : Raw

Advances p by n bytes. This is not an HAdd instance because it should be a relatively rare operation, so we use a name to make accidental use less likely. To add the size of a character c or string s to a raw position p, you can use p + c resp. p + s.

This should be seen as an "advance" or "skip".

See also Pos.Raw.offsetBy, which turns relative positions into absolute positions.

Equations

• p.increaseBy n = { byteIdx := p.byteIdx + n }

@[simp]

theorem String.Pos.Raw.byteIdx_increaseBy {p : Raw} {n : Nat} : (p.increaseBy n).byteIdx = p.byteIdx + n

@[inline]

def String.Pos.Raw.decreaseBy (p : Raw) (n : Nat) : Raw

Move the position p back by n bytes. This is not an HSub instance because it should be a relatively rare operation, so we use a name to make accidental use less likely. To remove the size of a character c or string s from a raw position p, you can use p - c resp. p - s.

This should be seen as the inverse of an "advance" or "skip".

See also Pos.Raw.unoffsetBy, which turns absolute positions into relative positions.

Equations

• p.decreaseBy n = { byteIdx := p.byteIdx - n }

@[simp]

theorem String.Pos.Raw.byteIdx_decreaseBy {p : Raw} {n : Nat} : (p.decreaseBy n).byteIdx = p.byteIdx - n

theorem String.Pos.Raw.increaseBy_charUtf8Size {p : Raw} {c : Char} : p.increaseBy c.utf8Size = p + c

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!" 2005 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

@[inline]

def String.Pos.Raw.inc (p : Raw) : Raw

Increases the byte offset of the position by 1. Not to be confused with ValidPos.next.

Equations

• p.inc = { byteIdx := p.byteIdx + 1 }

@[simp]

theorem String.Pos.Raw.byteIdx_inc {p : Raw} : p.inc.byteIdx = p.byteIdx + 1

@[inline]

def String.Pos.Raw.dec (p : Raw) : Raw

Decreases the byte offset of the position by 1. Not to be confused with ValidPos.prev.

Equations

• p.dec = { byteIdx := p.byteIdx - 1 }

@[simp]

theorem String.Pos.Raw.byteIdx_dec {p : Raw} : p.dec.byteIdx = p.byteIdx - 1

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

@[inline]

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 = (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

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

@[simp]

theorem String.Pos.Raw.le_refl {p : Raw} : p ≤ p

theorem String.Pos.Raw.lt_inc {p : Raw} : p < p.inc

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

theorem String.Pos.Raw.inc_le {p q : Raw} : p.inc ≤ q ↔ p < q

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.Pos.Raw.lt_of_le_of_lt {a b c : Raw} : a ≤ b → b < c → a < c

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

theorem String.Pos.Raw.ne_of_lt {a b : Raw} : a < b → a ≠ b

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

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

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

Advances the position p n times, saturating at s.endPos if necessary.

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, saturating at s.startPos if necessary.

Equations

• p.prevn 0 = p
• p.prevn n_2.succ = if h : p ≠ s.startPos then (p.prev h).prevn n_2 else 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.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.data 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.data 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✝¹.data 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✝¹.data 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.data 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.data 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.toSlice_get {s : String} {p : s.ValidPos} {h : p.toSlice ≠ s.toSlice.endPos} : p.toSlice.get h = p.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.byteIdx_lt_utf8ByteSize {s : String} (p : s.ValidPos) (h : p ≠ s.endValidPos) : p.offset.byteIdx < s.utf8ByteSize

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

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

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

@[extern lean_string_utf8_set]

def String.ValidPos.set {s : String} (p : s.ValidPos) (c : Char) (hp : p ≠ s.endValidPos) : String

Replaces the character at a specified position in a string with a new character.

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

Examples:

• ("abc".pos ⟨1⟩ (by decide)).set 'B' (by decide) = "aBc"
• ("L∃∀N".pos ⟨4⟩ (by decide)).set 'X' (by decide) = "L∃XN"

Equations

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

theorem String.ValidPos.set_eq_append {s : String} {p : s.ValidPos} {c : Char} {hp : p ≠ s.endValidPos} : p.set c hp = (s.replaceEnd p).copy ++ singleton c ++ (s.replaceStart (p.next hp)).copy

theorem String.Pos.Raw.IsValid.set_of_le {s : String} {p : s.ValidPos} {c : Char} {hp : p ≠ s.endValidPos} {q : Raw} (hq : IsValid s q) (hpq : q ≤ p.offset) : IsValid (p.set c hp) q

@[inline]

def String.ValidPos.setOfLE {s : String} (q p : s.ValidPos) (c : Char) (hp : p ≠ s.endValidPos) (hpq : q ≤ p) : (p.set c hp).ValidPos

Given a valid position in a string, obtain the corresponding position after setting a character on that string, provided that the position was before the changed position.

Equations

• q.setOfLE p c hp hpq = { offset := q.offset, isValid := ⋯ }

@[simp]

theorem String.ValidPos.offset_setOfLE {s : String} {q p : s.ValidPos} {c : Char} {hp : p ≠ s.endValidPos} {hpq : q ≤ p} : (q.setOfLE p c hp hpq).offset = q.offset

def String.ValidPos.modify {s : String} (p : s.ValidPos) (f : Char → Char) (hp : p ≠ s.endValidPos) : String

Replaces the character at position p in the string s with the result of applying f to that character.

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

Examples:

• ("abc".pos ⟨1⟩ (by decide)).modify Char.toUpper (by decide) = "aBc"

Equations

• p.modify f hp = p.set (f (p.get hp)) hp

theorem String.Pos.Raw.IsValid.modify_of_le {s : String} {p : s.ValidPos} {f : Char → Char} {hp : p ≠ s.endValidPos} {q : Raw} (hq : IsValid s q) (hpq : q ≤ p.offset) : IsValid (p.modify f hp) q

def String.ValidPos.modifyOfLE {s : String} (q p : s.ValidPos) (f : Char → Char) (hp : p ≠ s.endValidPos) (hpq : q ≤ p) : (p.modify f hp).ValidPos

Given a valid position in a string, obtain the corresponding position after modifying a character in that string, provided that the position was before the changed position.

Equations

• q.modifyOfLE p f hp hpq = { offset := q.offset, isValid := ⋯ }

@[simp]

theorem String.ValidPos.offset_modifyOfLE {s : String} {q p : s.ValidPos} {f : Char → Char} {hp : p ≠ s.endValidPos} {hpq : q ≤ p} : (q.modifyOfLE p f hp hpq).offset = q.offset

@[extern lean_string_utf8_set]

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

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

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

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

Examples:

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

Equations

• String.Pos.Raw.set x✝² x✝¹ x✝ = (String.Pos.Raw.utf8SetAux x✝ x✝².data 0 x✝¹).asString

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

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

Equations

• x✝².set x✝¹ x✝ = (String.Pos.Raw.utf8SetAux x✝ x✝².data 0 x✝¹).asString

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

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

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

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

Examples:

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

Equations

• String.Pos.Raw.modify s i f = String.Pos.Raw.set s i (f (String.Pos.Raw.get s i))

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

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

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

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

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

Examples:

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

Equations

• s.modify i f = String.Pos.Raw.set s i (f (String.Pos.Raw.get s i))

@[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 endPos, 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".endPos |> "abc".prev) = 'c'
• "L∃∀N".get ("L∃∀N".endPos |> "L∃∀N".prev |> "L∃∀N".prev |> "L∃∀N".prev) = '∃'

Equations

• String.Pos.Raw.prev x✝¹ x✝ = String.Pos.Raw.utf8PrevAux x✝¹.data 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✝¹.data 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.endPos)

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

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

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

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

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

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

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

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.endPos.

Examples:

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

Equations

• s.posOf c = s.posOfAux c s.endPos 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.endPos

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

@[reducible, inline]

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

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

Equations

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

@[export lean_string_pos_min]

def String.Pos.Raw.Internal.minImpl (p₁ p₂ : Raw) : Raw

Equations

• String.Pos.Raw.Internal.minImpl p₁ p₂ = p₁.min p₂

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.endPos.min b.endPos) 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.Pos.Raw.extract.go₁ x✝².data 0 x✝¹ x✝).asString

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

instance String.instInhabited_1 : Inhabited String

Equations

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

instance String.instAppend : Append String

Equations

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

@[inline]

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

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

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

Examples:

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

Equations

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

@[export lean_string_pushn]

def String.Internal.pushnImpl (s : String) (c : Char) (n : Nat) : String

Equations

• String.Internal.pushnImpl s c n = s.pushn c n

@[inline]

def String.isEmpty (s : String) : Bool

Checks whether a string is empty.

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

Examples:

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

Equations

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

@[export lean_string_isempty]

def String.Internal.isEmptyImpl (s : String) : Bool

Equations

• String.Internal.isEmptyImpl s = s.isEmpty

@[inline]

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

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

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

Examples:

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

Equations

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

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

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

Examples:

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

Equations

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

@[export lean_string_intercalate]

def String.Internal.intercalateImpl (s : String) : List String → String

Equations

• String.Internal.intercalateImpl s = s.intercalate

structure String.Iterator : Type

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

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

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

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

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

• s : String

  The string being iterated over.

• i : Pos.Raw

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

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

def String.instDecidableEqIterator.decEq (x✝ x✝¹ : Iterator) : Decidable (x✝ = x✝¹)

Equations

• String.instDecidableEqIterator.decEq { s := a, i := a_1 } { s := b, i := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance String.instDecidableEqIterator : DecidableEq Iterator

Equations

• String.instDecidableEqIterator = String.instDecidableEqIterator.decEq

def String.instInhabitedIterator.default : Iterator

Equations

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

instance String.instInhabitedIterator : Inhabited Iterator

Equations

• String.instInhabitedIterator = { default := String.instInhabitedIterator.default }

@[inline]

def String.mkIterator (s : String) : Iterator

Creates an iterator at the beginning of the string.

Equations

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

@[reducible, inline]

abbrev String.iter (s : String) : Iterator

Creates an iterator at the beginning of the string.

Equations

• String.iter = String.mkIterator

instance String.instSizeOfIterator : SizeOf Iterator

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

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

Equations

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

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

@[inline]

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

The string being iterated over.

Equations

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

@[inline]

def String.Iterator.remainingBytes : Iterator → Nat

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

Equations

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

@[inline]

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

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

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

Equations

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

@[inline]

def String.Iterator.curr : Iterator → Char

Gets the character at the iterator's current position.

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

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

Equations

• { s := s, i := i }.curr = String.Pos.Raw.get s i

@[inline]

def String.Iterator.next : Iterator → Iterator

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

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

Equations

• { s := s, i := i }.next = { s := s, i := String.Pos.Raw.next s i }

@[inline]

def String.Iterator.prev : Iterator → Iterator

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

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

Equations

• { s := s, i := i }.prev = { s := s, i := String.Pos.Raw.prev s i }

@[inline]

def String.Iterator.atEnd : Iterator → Bool

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

Equations

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

@[inline]

def String.Iterator.hasNext : Iterator → Bool

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

Equations

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

@[inline]

def String.Iterator.hasPrev : Iterator → Bool

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

Equations

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

@[inline]

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

Gets the character at the iterator's current position.

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

Equations

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

@[inline]

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

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

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

Equations

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

@[inline]

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

Replaces the current character in the string.

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

Equations

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

@[inline]

def String.Iterator.toEnd : Iterator → Iterator

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

Equations

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

@[inline]

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

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

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

Equations

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

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

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

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

Equations

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

@[inline]

def String.Iterator.remainingToString : Iterator → String

The remaining characters in an iterator, as a string.

Equations

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

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

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

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

Equations

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

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

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

Equations

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

@[irreducible]

def String.offsetOfPosAux (s : String) (pos i : Pos.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.endPos 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.endPos 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.endPos 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

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

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

@[irreducible, specialize #[]]

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

Equations

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

@[inline]

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

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

Examples:

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

Equations

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

@[inline]

def String.isNat (s : String) : Bool

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

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

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

Examples:

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

Equations

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

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

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

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

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

Examples:

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

Equations

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

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

@[export lean_string_isprefixof]

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

Equations

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

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

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

Examples:

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

Equations

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

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 }

@[inline]

def Substring.isEmpty (ss : Substring) : Bool

Checks whether a substring is empty.

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

Equations

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

@[export lean_substring_isempty]

def Substring.Internal.isEmptyImpl (ss : Substring) : Bool

Equations

• Substring.Internal.isEmptyImpl ss = ss.isEmpty

@[inline]

def Substring.toString : Substring → String

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

Equations

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

@[export lean_substring_tostring]

def Substring.Internal.toStringImpl : Substring → String

Equations

• Substring.Internal.toStringImpl = Substring.toString

@[inline]

def Substring.toIterator : Substring → String.Iterator

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

Equations

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

@[inline]

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

Returns the character at the given position in the substring.

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

Equations

• { str := s, startPos := b, stopPos := stopPos }.get x✝ = String.Pos.Raw.get s (x✝.offsetBy b)

@[export lean_substring_get]

def Substring.Internal.getImpl : Substring → String.Pos.Raw → Char

Equations

• Substring.Internal.getImpl = Substring.get

@[inline]

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

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

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

Equations

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

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

@[inline]

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

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

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

Equations

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

@[export lean_substring_prev]

def Substring.Internal.prevImpl : Substring → String.Pos.Raw → String.Pos.Raw

Equations

• Substring.Internal.prevImpl = Substring.prev

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

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

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

Equations

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

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

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

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

Equations

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

@[inline]

def Substring.front (s : Substring) : Char

Returns the first character in the substring.

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

Equations

• s.front = s.get 0

@[export lean_substring_front]

def Substring.Internal.frontImpl : Substring → Char

Equations

• Substring.Internal.frontImpl = Substring.front

@[inline]

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

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

Equations

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

@[inline]

def Substring.drop : Substring → Nat → Substring

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

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

Equations

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

@[export lean_substring_drop]

def Substring.Internal.dropImpl : Substring → Nat → Substring

Equations

• Substring.Internal.dropImpl = Substring.drop

@[inline]

def Substring.dropRight : Substring → Nat → Substring

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

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

Equations

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

@[inline]

def Substring.take : Substring → Nat → Substring

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

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

Equations

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

@[inline]

def Substring.takeRight : Substring → Nat → Substring

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

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

Equations

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

@[inline]

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

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

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

Equations

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

@[inline]

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

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

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

Equations

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

@[export lean_substring_extract]

def Substring.Internal.extractImpl : Substring → String.Pos.Raw → String.Pos.Raw → Substring

Equations

• Substring.Internal.extractImpl = Substring.extract

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

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

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

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

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

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

Equations

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

@[inline]

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

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

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

Equations

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

@[export lean_substring_all]

def Substring.Internal.allImpl (s : Substring) (p : Char → Bool) : Bool

Equations

• Substring.Internal.allImpl s p = s.all p

@[inline]

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

Checks whether a substring contains the specified character.

Equations

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

@[irreducible, specialize #[]]

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

Equations

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

@[inline]

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

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

Equations

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

@[export lean_substring_takewhile]

def Substring.Internal.takeWhileImpl : Substring → (Char → Bool) → Substring

Equations

• Substring.Internal.takeWhileImpl = Substring.takeWhile

@[inline]

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

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

Equations

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

@[irreducible, specialize #[]]

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

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

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

@[inline]

def Substring.trimLeft (s : Substring) : Substring

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

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

Equations

• s.trimLeft = s.dropWhile Char.isWhitespace

@[inline]

def Substring.trimRight (s : Substring) : Substring

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

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

Equations

• s.trimRight = s.dropRightWhile Char.isWhitespace

@[inline]

def Substring.trim : Substring → Substring

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

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

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

Examples:

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

Equations

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

@[inline]

def Substring.isNat (s : Substring) : Bool

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

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

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

Equations

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

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

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

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

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

Equations

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

def Substring.repair : Substring → Substring

Given a Substring, returns another one which has valid endpoints and represents the same substring according to Substring.toString. (Note, the substring may still be inverted, i.e. beginning greater than end.)

Equations

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

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

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

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

Equations

• ss1.beq ss2 = (ss1.repair.bsize == ss2.repair.bsize && String.Pos.Raw.substrEq ss1.repair.str ss1.repair.startPos ss2.repair.str ss2.repair.startPos ss1.repair.bsize)

@[export lean_substring_beq]

def Substring.Internal.beqImpl (ss1 ss2 : Substring) : Bool

Equations

• Substring.Internal.beqImpl ss1 ss2 = ss1.beq ss2

instance Substring.hasBeq : BEq Substring

Equations

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

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

Checks whether two substrings have the same position and content.

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

Equations

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

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

Returns the longest common prefix of two substrings.

The returned substring uses the same underlying string as s.

Equations

• s.commonPrefix t = { str := s.str, startPos := s.startPos, stopPos := Substring.commonPrefix.loop✝ s t s.startPos t.startPos }

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

Returns the longest common suffix of two substrings.

The returned substring uses the same underlying string as s.

Equations

• s.commonSuffix t = { str := s.str, startPos := Substring.commonSuffix.loop✝ s t s.stopPos t.stopPos, stopPos := s.stopPos }

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

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

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

Equations

• s.dropPrefix? pre = if (s.commonPrefix pre).bsize = pre.bsize then some { str := s.str, startPos := (s.commonPrefix pre).stopPos, stopPos := s.stopPos } else none

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

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

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

Equations

• s.dropSuffix? suff = if (s.commonSuffix suff).bsize = suff.bsize then some { str := s.str, startPos := s.startPos, stopPos := (s.commonSuffix suff).startPos } else none

@[inline]

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

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

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

Examples:

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

Equations

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

@[export lean_string_drop]

def String.Internal.dropImpl (s : String) (n : Nat) : String

Equations

• String.Internal.dropImpl s n = s.drop n

@[inline]

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

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

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

Examples:

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

Equations

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

@[export lean_string_dropright]

def String.Internal.dropRightImpl (s : String) (n : Nat) : String

Equations

• String.Internal.dropRightImpl s n = s.dropRight n

@[inline]

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

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

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

Examples:

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

Equations

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

@[inline]

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

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

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

Examples:

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

Equations

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

@[inline]

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

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

Examples:

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

Equations

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

@[inline]

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

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

Examples:

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

Equations

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

@[inline]

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

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

Examples:

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

Equations

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

@[inline]

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

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

Examples:

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

Equations

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

@[inline]

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

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

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

Examples:

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

Equations

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

@[inline]

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

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

Examples:

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

Equations

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

@[inline]

def String.trimRight (s : String) : String

Removes trailing whitespace from a string.

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

Examples:

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

Equations

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

@[inline]

def String.trimLeft (s : String) : String

Removes leading whitespace from a string.

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

Examples:

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

Equations

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

@[inline]

def String.trim (s : String) : String

Removes leading and trailing whitespace from a string.

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

Examples:

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

Equations

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

@[export lean_string_trim]

def String.Internal.trimImpl (s : String) : String

Equations

• String.Internal.trimImpl s = s.trim

@[inline]

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

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

Examples:

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

Equations

• String.Pos.Raw.nextWhile s p i = Substring.takeWhileAux s s.endPos p i

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

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

Equations

• s.nextWhile p i = String.Pos.Raw.nextWhile s p i

@[export lean_string_nextwhile]

def String.Internal.nextWhileImpl (s : String) (p : Char → Bool) (i : Pos.Raw) : Pos.Raw

Equations

• String.Internal.nextWhileImpl s p i = String.Pos.Raw.nextWhile s p i

@[inline]

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

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

Examples:

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

Equations

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

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

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

Equations

• s.nextUntil p i = String.Pos.Raw.nextUntil s p i

@[inline]

def String.toUpper (s : String) : String

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

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

Examples:

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

Equations

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

@[inline]

def String.toLower (s : String) : String

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

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

Examples:

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

Equations

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

@[inline]

def String.capitalize (s : String) : String

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

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

Examples:

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

Equations

• s.capitalize = String.Pos.Raw.set s 0 (String.Pos.Raw.get s 0).toUpper

@[export lean_string_capitalize]

def String.Internal.capitalizeImpl (s : String) : String

Equations

• String.Internal.capitalizeImpl s = s.capitalize

@[inline]

def String.decapitalize (s : String) : String

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

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

Examples:

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

Equations

• s.decapitalize = String.Pos.Raw.set s 0 (String.Pos.Raw.get s 0).toLower

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

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

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

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

Examples:

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

Equations

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

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

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

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

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

Examples:

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

Equations

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

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

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

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

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

Examples:

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

Equations

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

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

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

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

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

Examples:

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

Equations

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

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

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

@[simp]

theorem String.default_eq : default = ""

@[simp]

theorem String.mk_eq_asString (s : List Char) : mk s = s.asString

@[simp]

theorem String.length_empty : "".length = 0

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

@[simp]

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

@[simp]

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

theorem String.push_eq_append {s : String} (c : Char) : s.push c = s ++ singleton c

@[simp]

theorem String.data_push {s : String} (c : Char) : (s.push c).data = s.data ++ [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.data < t.data

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

@[simp]

theorem String.Pos.Raw.mk_zero : { } = 0

@[simp]

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

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

theorem String.Pos.Raw.add_byteIdx {p₁ p₂ : Raw} : (p₂.offsetBy p₁).byteIdx = p₁.byteIdx + p₂.byteIdx

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

theorem String.Pos.Raw.add_eq {p₁ p₂ : Raw} : p₂.offsetBy p₁ = { byteIdx := p₁.byteIdx + p₂.byteIdx }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations

• @String.Pos.Raw.addString_byteIdx = @String.Pos.Raw.byteIdx_add_string

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

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

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

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

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

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

Equations

• String.Pos.Raw.zero_addString_byteIdx = String.Pos.Raw.byteIdx_zero_add_string

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

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

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

@[simp]

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

@[simp]

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

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

theorem Char.toString_eq_singleton {c : Char} : c.toString = String.singleton c

@[simp]

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

@[simp]

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

@[simp]

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