@[inline]

def String.replace {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] {α : Type u_1} [ToSlice α] (s : String) (pattern : ρ) [Slice.Pattern.ToForwardSearcher pattern σ] (replacement : α) : String

Constructs a new string obtained by replacing all occurrences of pattern with replacement in s.

This function is generic over all currently supported patterns. The replacement may be a String or a String.Slice.

Examples:

• "red green blue".replace 'e' "" = "rd grn blu"

• "red green blue".replace (fun c => c == 'u' || c == 'e') "" = "rd grn bl"

• "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"

• "aaaaa".replace "aa" "b" = "bba"

• "abc".replace "" "k" = "kakbkck"

@[inline]

def String.Slice.Pos.find? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] {s : Slice} (pos : s.Pos) (pattern : ρ) [Pattern.ToForwardSearcher pattern σ] : Option s.Pos

Finds the position of the first match of the pattern pattern in after the position pos. If there is no match none is returned.

This function is generic over all currently supported patterns.

Examples:

• ("coffee tea water".toSlice.startPos.find? Char.isWhitespace).map (·.get!) == some ' '

• ("tea".toSlice.pos ⟨1⟩ (by decide)).find? (fun (c : Char) => c == 't') == none

@[inline]

def String.Slice.Pos.find {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] {s : Slice} (pos : s.Pos) (pattern : ρ) [Pattern.ToForwardSearcher pattern σ] : s.Pos

Finds the position of the first match of the pattern pattern in after the position pos. If there is no match s.endPos is returned.

This function is generic over all currently supported patterns.

Examples:

• ("coffee tea water".toSlice.startPos.find Char.isWhitespace).get! == ' '

• ("tea".toSlice.pos ⟨1⟩ (by decide)).find (fun (c : Char) => c == 't') == "tea".toSlice.endPos

@[inline]

def String.Pos.find? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] {s : String} (pos : s.Pos) (pattern : ρ) [Slice.Pattern.ToForwardSearcher pattern σ] : Option s.Pos

Finds the position of the first match of the pattern pattern in after the position pos. If there is no match none is returned.

This function is generic over all currently supported patterns.

Examples:

• ("coffee tea water".startPos.find? Char.isWhitespace).map (·.get!) == some ' '

• ("tea".pos ⟨1⟩ (by decide)).find? (fun (c : Char) => c == 't') == none

@[inline]

def String.Pos.find {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] {s : String} (pos : s.Pos) (pattern : ρ) [Slice.Pattern.ToForwardSearcher pattern σ] : s.Pos

Finds the position of the first match of the pattern pattern in after the position pos. If there is no match s.endPos is returned.

This function is generic over all currently supported patterns.

Examples:

• ("coffee tea water".startPos.find Char.isWhitespace).get! == ' '

• ("tea".pos ⟨1⟩ (by decide)).find (fun (c : Char) => c == 't') == "tea".endPos

@[inline]

def String.find? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] (s : String) (pattern : ρ) [Slice.Pattern.ToForwardSearcher pattern σ] : Option s.Pos

Finds the position of the first match of the pattern pattern in a string s. If there is no match none is returned.

This function is generic over all currently supported patterns.

Examples:

• ("coffee tea water".find? Char.isWhitespace).map (·.get!) == some ' '

• "tea".find? (fun (c : Char) => c == 'X') == none

• ("coffee tea water".find? "tea").map (·.get!) == some 't'

@[inline]

def String.find {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] (s : String) (pattern : ρ) [Slice.Pattern.ToForwardSearcher pattern σ] : s.Pos

Finds the position of the first match of the pattern pattern in a slice s. If there is no match s.endPos is returned.

This function is generic over all currently supported patterns.

Examples:

• ("coffee tea water".find Char.isWhitespace).get! == ' '

• "tea".find (fun (c : Char) => c == 'X') == "tea".endPos

• ("coffee tea water".find "tea").get! == 't'

@[inline]

def String.Slice.Pos.revFind? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] {s : Slice} (pos : s.Pos) (pattern : ρ) [Pattern.ToBackwardSearcher pattern σ] : Option s.Pos

Finds the position of the first match of the pattern pattern in a slice s that is strictly before pos. If there is no such match none is returned.

This function is generic over all currently supported patterns except String/String.Slice.

Examples:

• (("abc".toSlice.endPos.prev (by decide)).revFind? Char.isAlpha).map (·.get!) == some 'b'

• "abc".toSlice.startPos.revFind? Char.isAlpha == none

@[inline]

def String.Pos.revFind? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] {s : String} (pos : s.Pos) (pattern : ρ) [Slice.Pattern.ToBackwardSearcher pattern σ] : Option s.Pos

Finds the position of the first match of the pattern pattern in a slice s that is strictly before pos. If there is no such match none is returned.

This function is generic over all currently supported patterns except String/String.Slice.

Examples:

• (("ab1c".endPos.prev (by decide)).revFind? Char.isAlpha).map (·.get!) == some 'b'

• "abc".startPos.revFind? Char.isAlpha == none

@[inline]

def String.revFind? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] (s : String) (pattern : ρ) [Slice.Pattern.ToBackwardSearcher pattern σ] : Option s.Pos

Finds the position of the first match of the pattern pattern in a string, starting from the end of the slice and traversing towards the start. If there is no match none is returned.

This function is generic over all currently supported patterns except String/String.Slice.

Examples:

• ("coffee tea water".toSlice.revFind? Char.isWhitespace).map (·.get!) == some ' '

• "tea".toSlice.revFind? (fun (c : Char) => c == 'X') == none

@[export lean_string_posof]

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

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

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

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

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

@[deprecated String.find (since := "2025-11-19")]

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

@[deprecated String.Pos.revFind? (since := "2025-11-19")]

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

@[deprecated String.revFind? (since := "2025-11-19")]

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

@[deprecated String.Pos.revFind? (since := "2025-11-19")]

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

@[deprecated String.revFind? (since := "2025-11-19")]

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

@[deprecated String.Pos.revFind? (since := "2025-11-19")]

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.Raw or immediately after a '\n' character.

@[inline]

def String.split {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] (s : String) (pat : ρ) [Slice.Pattern.ToForwardSearcher pat σ] : Std.Iter Slice

Splits a string at each subslice that matches the pattern pat.

The subslices that matched the pattern are not included in any of the resulting subslices. If multiple subslices in a row match the pattern, the resulting list will contain empty strings.

This function is generic over all currently supported patterns.

Examples:

• ("coffee tea water".split Char.isWhitespace).toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]

• ("coffee tea water".split ' ').toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]

• ("coffee tea water".split " tea ").toList == ["coffee".toSlice, "water".toSlice]

• ("ababababa".split "aba").toList == ["coffee".toSlice, "water".toSlice]

• ("baaab".split "aa").toList == ["b".toSlice, "ab".toSlice]

@[inline]

def String.splitInclusive {ρ : Type} {σ : Slice → Type} (s : String) (pat : ρ) [Slice.Pattern.ToForwardSearcher pat σ] : Std.Iter Slice

Splits a string at each subslice that matches the pattern pat. Unlike split the matched subslices are included at the end of each subslice.

This function is generic over all currently supported patterns.

Examples:

• ("coffee tea water".splitInclusive Char.isWhitespace).toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]

• ("coffee tea water".splitInclusive ' ').toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]

• ("coffee tea water".splitInclusive " tea ").toList == ["coffee tea ".toSlice, "water".toSlice]

• ("baaab".splitInclusive "aa").toList == ["baa".toSlice, "ab".toSlice]

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

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

@[inline]

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

Folds a function over a string from the start, 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"

@[export lean_string_foldl]

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

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

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

@[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 => s.push c) "" = "retaw aet eeffoc"

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

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

@[inline]

def String.contains {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] (s : String) (pat : ρ) [Slice.Pattern.ToForwardSearcher pat σ] : Bool

Checks whether a string has a match of the pattern pat anywhere.

This function is generic over all currently supported patterns.

Examples:

• "coffee tea water".contains Char.isWhitespace = true

• "tea".contains (fun (c : Char) => c == 'X') = false

• "coffee tea water".contains "tea" = true

@[export lean_string_contains]

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

@[inline]

def String.any {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] (s : String) (pat : ρ) [Slice.Pattern.ToForwardSearcher pat σ] : Bool

Checks whether a string has a match of the pattern pat anywhere.

This function is generic over all currently supported patterns.

Examples:

• "coffee tea water".contains Char.isWhitespace = true

• "tea".contains (fun (c : Char) => c == 'X') = false

• "coffee tea water".contains "tea" = true

@[export lean_string_any]

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

@[inline]

def String.all {ρ : Type} (s : String) (pat : ρ) [Slice.Pattern.ForwardPattern pat] : Bool

Checks whether a slice only consists of matches of the pattern pat.

Short-circuits at the first pattern mis-match.

This function is generic over all currently supported patterns.

Examples:

• "brown".all Char.isLower = true

• "brown and orange".all Char.isLower = false

• "aaaaaa".all 'a' = true

• "aaaaaa".all "aa" = true

• "aaaaaaa".all "aa" = false

@[inline]

def String.isNat (s : String) : Bool

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

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

Use toNat? or toNat! to convert such a slice 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

@[inline]

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

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

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

Use isNat to check whether toNat? would return some. toNat! is an alternative that panics instead of returning none when the slice 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

@[inline]

def String.toNat! (s : String) : Nat

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

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

Use isNat to check whether toNat! would return a value. toNat? is a safer alternative that returns none instead of panicking when the string is not a natural number.

Examples:

• "0".toNat! = 0

• "5".toNat! = 5

• "587".toNat! = 587

@[inline]

def String.toInt? (s : String) : Option Int

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

A string can be interpreted as a decimal integer if it only consists of at least one decimal digit and optionally - in front. Leading + characters are not allowed.

Use String.isInt to check whether String.toInt? would return some. String.toInt! is an alternative that panics instead of returning none when the string is not an integer.

Examples:

• "".toInt? = none

• "-".toInt? = none

• "0".toInt? = some 0

• "5".toInt? = some 5

• "-5".toInt? = some (-5)

• "587".toInt? = some 587

• "-587".toInt? = some (-587)

• " 5".toInt? = none

• "2-3".toInt? = none

• "0xff".toInt? = none

@[inline]

def String.isInt (s : String) : Bool

Checks whether the string can be interpreted as the decimal representation of an integer.

A string can be interpreted as a decimal integer if it only consists of at least one decimal digit and optionally - in front. Leading + characters are not allowed.

Use String.toInt? or String.toInt! to convert such a string to an integer.

Examples:

• "".isInt = false

• "-".isInt = false

• "0".isInt = true

• "-0".isInt = true

• "5".isInt = true

• "587".isInt = true

• "-587".isInt = true

• "+587".isInt = false

• " 5".isInt = false

• "2-3".isInt = false

• "0xff".isInt = false

@[inline]

def String.toInt! (s : String) : Int

Interprets a string as the decimal representation of an integer, returning it. Panics if the string does not contain a decimal integer.

A string can be interpreted as a decimal integer if it only consists of at least one decimal digit and optionally - in front. Leading + characters are not allowed.

Use String.isInt to check whether String.toInt! would return a value. String.toInt? is a safer alternative that returns none instead of panicking when the string is not an integer.

Examples:

• "0".toInt! = 0

• "5".toInt! = 5

• "587".toInt! = 587

• "-587".toInt! = -587

@[inline]

def String.front? (s : String) : Option Char

Returns the first character in s. If s is empty, returns none.

Examples:

• "abc".front? = some 'a'

• "".front? = none

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

@[export lean_string_front]

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

@[inline]

def String.back? (s : String) : Option Char

Returns the last character in s. If s is empty, returns none.

Examples:

• "abc".back? = some 'c'

• "".back? = none

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

def String.lines (s : String) : Std.Iter Slice

Creates an iterator over all lines in s with the line ending characters \r\n or \n being stripped.

Examples:

• "foo\r\nbar\n\nbaz\n".lines.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]

• "foo\r\nbar\n\nbaz".lines.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]

• "foo\r\nbar\n\nbaz\r".lines.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz\r".toSlice]