@[inline]

def String.replace {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.Iterators.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"

Equations

• s.replace pattern replacement = s.toSlice.replace pattern replacement

@[inline]

def String.Slice.Pos.find? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [(s : Slice) → Std.Iterators.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

Equations

• pos.find? pattern = Option.map String.Slice.Pos.ofSliceFrom ((s.sliceFrom pos).find? pattern)

@[inline]

def String.Slice.Pos.find {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [(s : Slice) → Std.Iterators.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

Equations

• pos.find pattern = String.Slice.Pos.ofSliceFrom ((s.sliceFrom pos).find pattern)

@[inline]

def String.Pos.find? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.Iterators.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

Equations

• pos.find? pattern = Option.map String.Pos.ofToSlice (pos.toSlice.find? pattern)

@[inline]

def String.Pos.find {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.Iterators.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

Equations

• pos.find pattern = String.Pos.ofToSlice (pos.toSlice.find pattern)

@[inline]

def String.find? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.Iterators.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'

Equations

• s.find? pattern = s.startPos.find? pattern

@[inline]

def String.find {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.Iterators.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'

Equations

• s.find pattern = s.startPos.find pattern

@[inline]

def String.Slice.Pos.revFind? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [(s : Slice) → Std.Iterators.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

Equations

• pos.revFind? pattern = Option.map String.Slice.Pos.ofSliceTo ((s.sliceTo pos).revFind? pattern)

@[inline]

def String.Pos.revFind? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.Iterators.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

Equations

• pos.revFind? pattern = Option.map String.Pos.ofToSlice (pos.toSlice.revFind? pattern)

@[inline]

def String.revFind? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.Iterators.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

Equations

• s.revFind? pattern = s.endPos.revFind? pattern

@[export lean_string_posof]

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

Equations

• String.Internal.posOfImpl s c = (s.find c).offset

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

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.

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

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.

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

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

Equations

• s.posOf c = (s.find c).offset

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

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

Equations

• s.revPosOfAux c pos = Option.map (fun (x : s.Pos) => x.offset) ((s.pos? pos).bind fun (x : s.Pos) => x.revFind? c)

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

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

Equations

• s.revPosOf c = Option.map (fun (x : s.Pos) => x.offset) (s.revFind? c)

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

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

Equations

• s.revFindAux p pos = Option.map (fun (x : s.Pos) => x.offset) ((s.pos? pos).bind fun (x : s.Pos) => x.revFind? p)

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

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

Equations

• s.revFind p = Option.map (fun (x : s.Pos) => x.offset) (s.revFind? p)

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

Equations

• s.findLineStart pos = (Option.map (fun (x : s.Pos) => x.offset) ((s.pos? pos).bind fun (x : s.Pos) => x.revFind? '\n')).getD s.startPos.offset

@[inline]

def String.split {ρ : Type} {σ : Slice → Type} (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]

Equations

• s.split pat = s.toSlice.split pat

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

Equations

• s.splitInclusive pat = s.toSlice.splitInclusive pat

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

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

Equations

• String.foldlAux f s stopPos i a = String.Slice.foldl f a (s.slice! (s.pos! i) (s.pos! stopPos))

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

Equations

• String.foldl f init s = String.Slice.foldl f init s.toSlice

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

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

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

Equations

• String.foldrAux f a s i begPos = String.Slice.foldr f a (s.slice! (s.pos! begPos) (s.pos! i))

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

Equations

• String.foldr f init s = String.Slice.foldr f init s.toSlice

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

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

Equations

• s.anyAux stopPos p i = (s.slice! (s.pos! i) (s.pos! stopPos)).any p

@[inline]

def String.contains {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.Iterators.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

Equations

• s.contains pat = s.toSlice.contains pat

@[export lean_string_contains]

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

Equations

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

@[inline]

def String.any {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.Iterators.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

Equations

• s.any pat = s.contains pat

@[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 {ρ : 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

Equations

• s.all pat = s.toSlice.all pat

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

Equations

• s.isNat = s.toSlice.isNat

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

Equations

• s.toNat? = s.toSlice.toNat?

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

Equations

• s.toNat! = s.toSlice.toNat!

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

Equations

• s.toInt? = s.toSlice.toInt?

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

Equations

• s.isInt = s.toSlice.isInt

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

Equations

• s.toInt! = s.toSlice.toInt!

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

Equations

• s.front? = s.toSlice.front?

@[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 = s.toSlice.front

@[export lean_string_front]

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

Equations

• String.Internal.frontImpl s = s.front

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

Equations

• s.back? = s.toSlice.back?

@[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 = s.toSlice.back

theorem String.Pos.ofToSlice_ne_endPos {s : String} {p : s.toSlice.Pos} (h : p ≠ s.toSlice.endPos) : ofToSlice p ≠ s.endPos

@[inline]

def String.Internal.toSliceWithProof {s : String} : { p : s.toSlice.Pos // p ≠ s.toSlice.endPos } → { p : s.Pos // p ≠ s.endPos }

Equations

• String.Internal.toSliceWithProof ⟨p, h⟩ = ⟨String.Pos.ofToSlice p, ⋯⟩

@[inline]

def String.positions (s : String) : Std.Iter { p : s.Pos // p ≠ s.endPos }

Creates an iterator over all valid positions within s.

Examples

• ("abc".positions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['a', 'b', 'c']

• ("abc".positions.map (·.val.offset.byteIdx) |>.toList) = [0, 1, 2]

• ("ab∀c".positions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['a', 'b', '∀', 'c']

• ("ab∀c".positions.map (·.val.offset.byteIdx) |>.toList) = [0, 1, 2, 5]

Equations

• s.positions = Std.Iterators.Iter.map String.Internal.toSliceWithProof s.toSlice.positions

@[inline]

def String.chars (s : String) : Std.Iter Char

Creates an iterator over all characters (Unicode code points) in s.

Examples:

• "abc".chars.toList = ['a', 'b', 'c']

• "ab∀c".chars.toList = ['a', 'b', '∀', 'c']

Equations

• s.chars = s.toSlice.chars

@[inline]

def String.revPositions (s : String) : Std.Iter { p : s.Pos // p ≠ s.endPos }

Creates an iterator over all valid positions within s, starting from the last valid position and iterating towards the first one.

Examples

• ("abc".revPositions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['c', 'b', 'a']

• ("abc".revPositions.map (·.val.offset.byteIdx) |>.toList) = [2, 1, 0]

• ("ab∀c".revPositions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['c', '∀', 'b', 'a']

• ("ab∀c".toSlice.revPositions.map (·.val.offset.byteIdx) |>.toList) = [5, 2, 1, 0]

Equations

• s.revPositions = Std.Iterators.Iter.map String.Internal.toSliceWithProof s.toSlice.revPositions

@[inline]

def String.revChars (s : String) : Std.Iter Char

Creates an iterator over all characters (Unicode code points) in s, starting from the end of the slice and iterating towards the start.

Example:

• "abc".revChars.toList = ['c', 'b', 'a']

• "ab∀c".revChars.toList = ['c', '∀', 'b', 'a']

Equations

• s.revChars = s.toSlice.revChars

@[inline]

def String.byteIterator (s : String) : Std.Iter UInt8

Creates an iterator over all bytes in s.

Examples:

• "abc".byteIterator.toList = [97, 98, 99]

• "ab∀c".byteIterator.toList = [97, 98, 226, 136, 128, 99]

Equations

• s.byteIterator = s.toSlice.bytes

@[inline]

def String.revBytes (s : String) : Std.Iter UInt8

Creates an iterator over all bytes in s, starting from the last one and iterating towards the first one.

Examples:

• "abc".revBytes.toList = [99, 98, 97]

• "ab∀c".revBytes.toList = [99, 128, 136, 226, 98, 97]

Equations

• s.revBytes = s.toSlice.revBytes

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]

Equations

• s.lines = s.toSlice.lines