Modification operations on strings

This file contains operations on strings which modify the string, like set or map. There will usually not be a String.Slice version of these operations.

@[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.toSetOfLE {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.toSetOfLE p c hp hpq = { offset := q.offset, isValid := ⋯ }

@[simp]

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

theorem String.Pos.Raw.isValid_add_char_set {s : String} {p : s.ValidPos} {c : Char} {hp : p ≠ s.endValidPos} : IsValid (p.set c hp) (p.offset + c)

@[inline]

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

The position just after the position that changed in a ValidPos.set call.

Equations

• p.pastSet c hp = { offset := p.offset + c, isValid := ⋯ }

@[simp]

theorem String.ValidPos.offset_pastSet {s : String} {p : s.ValidPos} {c : Char} {hp : p ≠ s.endValidPos} : (p.pastSet c hp).offset = p.offset + c

@[inline]

def String.ValidPos.appendRight {s : String} (p : s.ValidPos) (t : String) : (s ++ t).ValidPos

Equations

• p.appendRight t = { offset := p.offset, isValid := ⋯ }

theorem String.ValidPos.splits_pastSet {s : String} {p : s.ValidPos} {c : Char} {hp : p ≠ s.endValidPos} : (p.pastSet c hp).Splits ((s.replaceEnd p).copy ++ singleton c) (s.replaceStart (p.next hp)).copy

theorem String.remainingBytes_pastSet {s : String} {p : s.ValidPos} {c : Char} {hp : p ≠ s.endValidPos} : (p.pastSet c hp).remainingBytes = (p.next hp).remainingBytes

@[inline]

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

@[inline]

def String.ValidPos.toModifyOfLE {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.toModifyOfLE p f hp hpq = { offset := q.offset, isValid := ⋯ }

@[simp]

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

@[inline]

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

The position just after the position that was modified in a ValidPos.modify call.

Equations

• p.pastModify f hp = p.pastSet (f (p.get hp)) hp

theorem String.remainingBytes_pastModify {s : String} {p : s.ValidPos} {f : Char → Char} {hp : p ≠ s.endValidPos} : (p.pastModify f hp).remainingBytes = (p.next hp).remainingBytes

@[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.ofList (String.Pos.Raw.utf8SetAux x✝ x✝².toList 0 x✝¹)

@[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.ofList (String.Pos.Raw.utf8SetAux x✝ x✝².toList 0 x✝¹)

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

@[irreducible, specialize #[]]

def String.mapAux (f : Char → Char) (s : String) (p : s.ValidPos) : String

Equations

• String.mapAux f s p = if h : p = s.endValidPos then s else String.mapAux f (p.modify f h) (p.pastModify f h)

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

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