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.Pos.set {s : String} (p : s.Pos) (c : Char) (hp : p ≠ s.endPos) : 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"

theorem String.Pos.set_eq_append {s : String} {p : s.Pos} {c : Char} {hp : p ≠ s.endPos} : p.set c hp = (s.sliceTo p).copy ++ singleton c ++ (s.sliceFrom (p.next hp)).copy

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

@[inline]

def String.Pos.toSetOfLE {s : String} (q p : s.Pos) (c : Char) (hp : p ≠ s.endPos) (hpq : q ≤ p) : (p.set c hp).Pos

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.

@[simp]

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

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

@[inline]

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

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

@[simp]

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

@[inline]

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

theorem String.Pos.splits_pastSet {s : String} {p : s.Pos} {c : Char} {hp : p ≠ s.endPos} : (p.pastSet c hp).Splits ((s.sliceTo p).copy ++ singleton c) (s.sliceFrom (p.next hp)).copy

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

@[inline]

def String.Pos.modify {s : String} (p : s.Pos) (f : Char → Char) (hp : p ≠ s.endPos) : 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"

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

@[inline]

def String.Pos.toModifyOfLE {s : String} (q p : s.Pos) (f : Char → Char) (hp : p ≠ s.endPos) (hpq : q ≤ p) : (p.modify f hp).Pos

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.

@[simp]

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

@[inline]

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

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

theorem String.remainingBytes_pastModify {s : String} {p : s.Pos} {f : Char → Char} {hp : p ≠ s.endPos} : (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.Pos.set, combined with String.pos or another means of obtaining a String.Pos.

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.

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

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

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

Examples:

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

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

Examples:

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

@[irreducible, specialize #[]]

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

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

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

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

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

@[export lean_string_capitalize]

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

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