instance String.Slice.instHAppend : HAppend String Slice String

@[inline]

def String.Slice.isEmpty (s : Slice) : Bool

Checks whether a slice is empty.

Empty slices have utf8ByteSize 0.

Examples:

• "".toSlice.isEmpty = true

• " ".toSlice.isEmpty = false

def String.Slice.beq (s1 s2 : Slice) : Bool

Checks whether s1 and s2 represent the same string, even if they are slices of different base strings or different slices within the same string.

The implementation is an efficient equivalent of s1.copy == s2.copy

instance String.Slice.instBEq : BEq Slice

@[extern lean_slice_hash]

opaque String.Slice.hash (s : Slice) : UInt64

instance String.Slice.instHashable : Hashable Slice

instance String.Slice.instLT : LT Slice

@[extern lean_slice_dec_lt]

instance String.Slice.instDecidableLt (x y : Slice) : Decidable (x < y)

instance String.Slice.instOrd : Ord Slice

instance String.Slice.instLE : LE Slice

instance String.Slice.instDecidableLE : DecidableLE Slice

@[inline]

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

Checks whether the slice (s) begins with the pattern (pat).

This function is generic over all currently supported patterns.

Examples:

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

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

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

• "red green blue".toSlice.startsWith 'r' = true

• "red green blue".toSlice.startsWith Char.isLower = true

inductive String.Slice.SplitIterator {σ : Slice → Type} {ρ : Type} (pat : ρ) (s : Slice) [Pattern.ToForwardSearcher pat σ] : Type

• operating {σ : Slice → Type} {ρ : Type} {pat : ρ} {s : Slice} [Pattern.ToForwardSearcher pat σ] (currPos : s.Pos) (searcher : Std.Iter (Pattern.SearchStep s)) : SplitIterator pat s
• atEnd {σ : Slice → Type} {ρ : Type} {pat : ρ} {s : Slice} [Pattern.ToForwardSearcher pat σ] : SplitIterator pat s

instance String.Slice.instInhabitedSplitIterator {a✝ : Slice → Type} {a✝¹ : Type} {a✝² : a✝¹} {a✝³ : Slice} {a✝⁴ : Pattern.ToForwardSearcher a✝² a✝} : Inhabited (SplitIterator a✝² a✝³)

def String.Slice.instInhabitedSplitIterator.default {a✝ : Slice → Type} {a✝¹ : Type} {a✝² : a✝¹} {a✝³ : Slice} {a✝⁴ : Pattern.ToForwardSearcher a✝² a✝} : SplitIterator a✝² a✝³

inductive String.Slice.SplitIterator.PlausibleStep : Type

instance String.Slice.SplitIterator.instIteratorId {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] {pat : ρ} [Pattern.ToForwardSearcher pat σ] {s : Slice} : Std.Iterator (SplitIterator pat s) Id Slice

instance String.Slice.SplitIterator.instFiniteIdOfSearchStep {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] {pat : ρ} [Pattern.ToForwardSearcher pat σ] {s : Slice} [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (SplitIterator pat s) Id

instance String.Slice.SplitIterator.instIteratorLoopIdOfMonad {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] {pat : ρ} [Pattern.ToForwardSearcher pat σ] {n : Type u_1 → Type u_2} {s : Slice} [Monad n] : Std.IteratorLoop (SplitIterator pat s) Id n

@[specialize #[3]]

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

Splits a slice 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".toSlice.split Char.isWhitespace).toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]

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

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

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

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

inductive String.Slice.SplitInclusiveIterator {σ : Slice → Type} {ρ : Type} (pat : ρ) (s : Slice) [Pattern.ToForwardSearcher pat σ] : Type

• operating {σ : Slice → Type} {ρ : Type} {pat : ρ} {s : Slice} [Pattern.ToForwardSearcher pat σ] (currPos : s.Pos) (searcher : Std.Iter (Pattern.SearchStep s)) : SplitInclusiveIterator pat s
• atEnd {σ : Slice → Type} {ρ : Type} {pat : ρ} {s : Slice} [Pattern.ToForwardSearcher pat σ] : SplitInclusiveIterator pat s

def String.Slice.instInhabitedSplitInclusiveIterator.default {a✝ : Slice → Type} {a✝¹ : Type} {a✝² : a✝¹} {a✝³ : Slice} {a✝⁴ : Pattern.ToForwardSearcher a✝² a✝} : SplitInclusiveIterator a✝² a✝³

instance String.Slice.instInhabitedSplitInclusiveIterator {a✝ : Slice → Type} {a✝¹ : Type} {a✝² : a✝¹} {a✝³ : Slice} {a✝⁴ : Pattern.ToForwardSearcher a✝² a✝} : Inhabited (SplitInclusiveIterator a✝² a✝³)

instance String.Slice.SplitInclusiveIterator.instIteratorId {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] {pat : ρ} [Pattern.ToForwardSearcher pat σ] {s : Slice} : Std.Iterator (SplitInclusiveIterator pat s) Id Slice

instance String.Slice.SplitInclusiveIterator.instFiniteIdOfSearchStep {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] {pat : ρ} [Pattern.ToForwardSearcher pat σ] {s : Slice} [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (SplitInclusiveIterator pat s) Id

instance String.Slice.SplitInclusiveIterator.instIteratorLoopIdOfMonad {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] {pat : ρ} [Pattern.ToForwardSearcher pat σ] {n : Type u_1 → Type u_2} [Monad n] {s : Slice} : Std.IteratorLoop (SplitInclusiveIterator pat s) Id n

@[specialize #[3]]

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

Splits a slice 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".toSlice.splitInclusive Char.isWhitespace).toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]

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

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

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

@[inline]

def String.Slice.dropPrefix? {ρ : Type} (s : Slice) (pat : ρ) [Pattern.ForwardPattern pat] : Option Slice

If pat matches a prefix of s, returns the remainder. Returns none otherwise.

Use String.Slice.dropPrefix to return the slice unchanged when pat does not match a prefix.

This function is generic over all currently supported patterns.

Examples:

• "red green blue".toSlice.dropPrefix? "red " == some "green blue".toSlice

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

• "red green blue".toSlice.dropPrefix? 'r' == some "ed green blue".toSlice

• "red green blue".toSlice.dropPrefix? Char.isLower == some "ed green blue".toSlice

@[specialize #[2]]

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

If pat matches a prefix of s, returns the remainder. Returns s unmodified otherwise.

Use String.Slice.dropPrefix? to return none when pat does not match a prefix.

This function is generic over all currently supported patterns.

Examples:

• "red green blue".toSlice.dropPrefix "red " == "green blue".toSlice

• "red green blue".toSlice.dropPrefix "reed " == "red green blue".toSlice

• "red green blue".toSlice.dropPrefix 'r' == "ed green blue".toSlice

• "red green blue".toSlice.dropPrefix Char.isLower == "ed green blue".toSlice

def String.Slice.replace {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] {α : Type u_1} [ToSlice α] (s : Slice) (pattern : ρ) [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".toSlice.replace 'e' "" = "rd grn blu"

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

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

• "red green blue".toSlice.replace "ee" "E" = "red grEn blue"

• "red green blue".toSlice.replace "e" "E" = "rEd grEEn bluE"

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

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

@[inline]

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

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

If n is greater than the amount of characters in s, returns an empty slice.

Examples:

• "red green blue".toSlice.drop 4 == "green blue".toSlice

• "red green blue".toSlice.drop 10 == "blue".toSlice

• "red green blue".toSlice.drop 50 == "".toSlice

@[inline]

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

Creates a new slice that contains the longest prefix of s for which pat matched (potentially repeatedly).

Examples:

• "red green blue".toSlice.dropWhile Char.isLower == " green blue".toSlice

• "red green blue".toSlice.dropWhile 'r' == "ed green blue".toSlice

• "red red green blue".toSlice.dropWhile "red " == "green blue".toSlice

• "red green blue".toSlice.dropWhile (fun (_ : Char) => true) == "".toSlice

@[inline]

def String.Slice.trimAsciiStart (s : Slice) : Slice

Removes leading whitespace from a slice 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.

Examples:

• "abc".toSlice.trimAsciiStart == "abc".toSlice

• " abc".toSlice.trimAsciiStart == "abc".toSlice

• "abc \t ".toSlice.trimAsciiStart == "abc \t ".toSlice

• " abc ".toSlice.trimAsciiStart == "abc ".toSlice

• "abc\ndef\n".toSlice.trimAsciiStart == "abc\ndef\n".toSlice

@[inline]

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

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

If n is greater than the amount of characters in s, returns s.

Examples:

• "red green blue".toSlice.take 3 == "red".toSlice

• "red green blue".toSlice.take 1 == "r".toSlice

• "red green blue".toSlice.take 0 == "".toSlice

• "red green blue".toSlice.take 100 == "red green blue".toSlice

@[inline]

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

Creates a new slice that contains the longest prefix of s for which pat matched (potentially repeatedly).

This function is generic over all currently supported patterns.

Examples:

• "red green blue".toSlice.takeWhile Char.isLower == "red".toSlice

• "red green blue".toSlice.takeWhile 'r' == "r".toSlice

• "red red green blue".toSlice.takeWhile "red " == "red red ".toSlice

• "red green blue".toSlice.takeWhile (fun (_ : Char) => true) == "red green blue".toSlice

@[inline]

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

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

This function is generic over all currently supported patterns.

Examples:

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

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

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

@[inline]

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

Finds the position of the first match of the pattern pat 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".toSlice.find Char.isWhitespace).get! == ' '

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

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

@[specialize #[5]]

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

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

This function is generic over all currently supported patterns.

Examples:

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

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

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

@[inline]

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

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

This function is generic over all currently supported patterns.

Examples:

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

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

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

@[inline]

def String.Slice.all {ρ : Type} (s : Slice) (pat : ρ) [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".toSlice.all Char.isLower = true

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

• "aaaaaa".toSlice.all 'a' = true

• "aaaaaa".toSlice.all "aa" = true

• "aaaaaaa".toSlice.all "aa" = false

@[inline]

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

Checks whether the slice (s) ends with the pattern (pat).

This function is generic over all currently supported patterns.

Examples:

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

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

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

• "red green blue".toSlice.endsWith 'e' = true

• "red green blue".toSlice.endsWith Char.isLower = true

inductive String.Slice.RevSplitIterator {σ : Slice → Type} {ρ : Type} (pat : ρ) (s : Slice) [Pattern.ToBackwardSearcher pat σ] : Type

• operating {σ : Slice → Type} {ρ : Type} {pat : ρ} {s : Slice} [Pattern.ToBackwardSearcher pat σ] (currPos : s.Pos) (searcher : Std.Iter (Pattern.SearchStep s)) : RevSplitIterator pat s
• atEnd {σ : Slice → Type} {ρ : Type} {pat : ρ} {s : Slice} [Pattern.ToBackwardSearcher pat σ] : RevSplitIterator pat s

instance String.Slice.instInhabitedRevSplitIterator {a✝ : Slice → Type} {a✝¹ : Type} {a✝² : a✝¹} {a✝³ : Slice} {a✝⁴ : Pattern.ToBackwardSearcher a✝² a✝} : Inhabited (RevSplitIterator a✝² a✝³)

def String.Slice.instInhabitedRevSplitIterator.default {a✝ : Slice → Type} {a✝¹ : Type} {a✝² : a✝¹} {a✝³ : Slice} {a✝⁴ : Pattern.ToBackwardSearcher a✝² a✝} : RevSplitIterator a✝² a✝³

instance String.Slice.RevSplitIterator.instIteratorOfPure {ρ✝ : Type} {ρ : ρ✝} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] [Pattern.ToBackwardSearcher ρ σ] {m : Type → Type u_1} {s : Slice} [Pure m] : Std.Iterator (RevSplitIterator ρ s) m Slice

instance String.Slice.RevSplitIterator.instFiniteIdOfSearchStep {ρ✝ : Type} {ρ : ρ✝} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] [Pattern.ToBackwardSearcher ρ σ] {s : Slice} [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (RevSplitIterator ρ s) Id

instance String.Slice.RevSplitIterator.instIteratorLoopOfMonad {ρ✝ : Type} {ρ : ρ✝} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] [Pattern.ToBackwardSearcher ρ σ] {m : Type → Type u_1} {n : Type u_2 → Type u_3} {s : Slice} [Monad m] [Monad n] : Std.IteratorLoop (RevSplitIterator ρ s) m n

@[specialize #[3]]

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

Splits a slice at each subslice that matches the pattern pat, starting from the end of the slice and traversing towards the start.

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

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

Examples:

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

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

@[inline]

def String.Slice.dropSuffix? {ρ : Type} (s : Slice) (pat : ρ) [Pattern.BackwardPattern pat] : Option Slice

If pat matches a suffix of s, returns the remainder. Returns none otherwise.

Use String.Slice.dropSuffix to return the slice unchanged when pat does not match a prefix.

This function is generic over all currently supported patterns.

Examples:

• "red green blue".toSlice.dropSuffix? " blue" == some "red green".toSlice

• "red green blue".toSlice.dropSuffix? "bluu " == none

• "red green blue".toSlice.dropSuffix? 'e' == some "red green blu".toSlice

• "red green blue".toSlice.dropSuffix? Char.isLower == some "red green blu".toSlice

@[specialize #[2]]

def String.Slice.dropSuffix {ρ : Type} (s : Slice) (pat : ρ) [Pattern.BackwardPattern pat] : Slice

If pat matches a suffix of s, returns the remainder. Returns s unmodified otherwise.

Use String.Slice.dropSuffix? to return none when pat does not match a prefix.

This function is generic over all currently supported patterns.

Examples:

• "red green blue".toSlice.dropSuffix " blue" == "red green".toSlice

• "red green blue".toSlice.dropSuffix "bluu " == "red green blue".toSlice

• "red green blue".toSlice.dropSuffix 'e' == "red green blu".toSlice

• "red green blue".toSlice.dropSuffix Char.isLower == "red green blu".toSlice

@[inline]

def String.Slice.dropEnd (s : Slice) (n : Nat) : Slice

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

If n is greater than the amount of characters in s, returns an empty slice.

Examples:

• "red green blue".toSlice.dropEnd 5 == "red green".toSlice

• "red green blue".toSlice.dropEnd 11 == "red".toSlice

• "red green blue".toSlice.dropEnd 50 == "".toSlice

@[inline]

def String.Slice.dropEndWhile {ρ : Type} (s : Slice) (pat : ρ) [Pattern.BackwardPattern pat] : Slice

Creates a new slice that contains the longest suffix of s for which pat matched (potentially repeatedly).

Examples:

• "red green blue".toSlice.dropEndWhile Char.isLower == "red green ".toSlice

• "red green blue".toSlice.dropEndWhile 'e' == "red green blu".toSlice

• "red green blue".toSlice.dropEndWhile (fun (_ : Char) => true) == "".toSlice

@[inline]

def String.Slice.trimAsciiEnd (s : Slice) : Slice

Removes trailing whitespace from a slice 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.

Examples:

• "abc".toSlice.trimAsciiEnd == "abc".toSlice

• " abc".toSlice.trimAsciiEnd == " abc".toSlice

• "abc \t ".toSlice.trimAsciiEnd == "abc".toSlice

• " abc ".toSlice.trimAsciiEnd == " abc".toSlice

• "abc\ndef\n".toSlice.trimAsciiEnd == "abc\ndef".toSlice

@[inline]

def String.Slice.takeEnd (s : Slice) (n : Nat) : Slice

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

If n is greater than the amount of characters in s, returns s.

Examples:

• "red green blue".toSlice.takeEnd 4 == "blue".toSlice

• "red green blue".toSlice.takeEnd 1 == "e".toSlice

• "red green blue".toSlice.takeEnd 0 == "".toSlice

• "red green blue".toSlice.takeEnd 100 == "red green blue".toSlice

@[inline]

def String.Slice.takeEndWhile {ρ : Type} (s : Slice) (pat : ρ) [Pattern.BackwardPattern pat] : Slice

Creates a new slice that contains the suffix prefix of s for which pat matched (potentially repeatedly).

This function is generic over all currently supported patterns.

Examples:

• "red green blue".toSlice.takeEndWhile Char.isLower == "blue".toSlice

• "red green blue".toSlice.takeEndWhile 'e' == "e".toSlice

• "red green blue".toSlice.takeEndWhile (fun (_ : Char) => true) == "red green blue".toSlice

@[specialize #[5]]

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

Finds the position of the first match of the pattern pat in a slice, 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

def String.Slice.trimAscii (s : Slice) : Slice

Removes leading and trailing whitespace from a slice.

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

Examples:

• "abc".toSlice.trimAscii == "abc".toSlice

• " abc".toSlice.trimAscii == "abc".toSlice

• "abc \t ".toSlice.trimAscii == "abc".toSlice

• " abc ".toSlice.trimAscii == "abc".toSlice

• "abc\ndef\n".toSlice.trimAscii == "abc\ndef".toSlice

def String.Slice.eqIgnoreAsciiCase (s1 s2 : Slice) : Bool

Checks whether s1 == s2 if ASCII upper/lowercase are ignored.

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

• currPos : s.Pos

instance String.Slice.instInhabitedPosIterator {a✝ : Slice} : Inhabited a✝.PosIterator

def String.Slice.instInhabitedPosIterator.default {a✝ : Slice} : a✝.PosIterator

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

Creates an iterator over all valid positions within {name}s.

Examples

• {lean}("abc".toSlice.positions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['a', 'b', 'c']
• {lean}("abc".toSlice.positions.map (·.val.offset.byteIdx) |>.toList) = [0, 1, 2]
• {lean}("ab∀c".toSlice.positions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['a', 'b', '∀', 'c']
• {lean}("ab∀c".toSlice.positions.map (·.val.offset.byteIdx) |>.toList) = [0, 1, 2, 5]

instance String.Slice.PosIterator.instIteratorSubtypePosNeEndPosOfPure {m : Type → Type u_1} {s : Slice} [Pure m] : Std.Iterator s.PosIterator m { p : s.Pos // p ≠ s.endPos }

instance String.Slice.PosIterator.instFiniteSubtypePosNeEndPos {m : Type → Type u_1} {s : Slice} [Pure m] : Std.Iterators.Finite s.PosIterator m

instance String.Slice.PosIterator.instIteratorLoopSubtypePosNeEndPosOfMonad {m : Type → Type u_1} {n : Type u_2 → Type u_3} {s : Slice} [Monad m] [Monad n] : Std.IteratorLoop s.PosIterator m n

@[inline]

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

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

Examples:

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

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

@[deprecated "There is no constant-time length function on slices. Use `s.positions.count` instead, or `isEmpty` if you only need to know whether the slice is empty." (since := "2025-11-20")]

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

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

• currPos : s.Pos

instance String.Slice.instInhabitedRevPosIterator {a✝ : Slice} : Inhabited a✝.RevPosIterator

def String.Slice.instInhabitedRevPosIterator.default {a✝ : Slice} : a✝.RevPosIterator

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

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

Examples

• {lean}("abc".toSlice.revPositions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['c', 'b', 'a']
• {lean}("abc".toSlice.revPositions.map (·.val.offset.byteIdx) |>.toList) = [2, 1, 0]
• {lean}("ab∀c".toSlice.revPositions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['c', '∀', 'b', 'a']
• {lean}("ab∀c".toSlice.revPositions.map (·.val.offset.byteIdx) |>.toList) = [5, 2, 1, 0]

instance String.Slice.RevPosIterator.instIteratorSubtypePosNeEndPosOfPure {m : Type → Type u_1} {s : Slice} [Pure m] : Std.Iterator s.RevPosIterator m { p : s.Pos // p ≠ s.endPos }

instance String.Slice.RevPosIterator.instFiniteSubtypePosNeEndPos {m : Type → Type u_1} {s : Slice} [Pure m] : Std.Iterators.Finite s.RevPosIterator m

instance String.Slice.RevPosIterator.instIteratorLoopSubtypePosNeEndPosOfMonad {m : Type → Type u_1} {n : Type u_2 → Type u_3} {s : Slice} [Monad m] [Monad n] : Std.IteratorLoop s.RevPosIterator m n

@[inline]

def String.Slice.revChars (s : Slice) : 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".toSlice.revChars.toList = ['c', 'b', 'a']

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

structure String.Slice.ByteIterator : Type

• s : Slice
• offset : Pos.Raw

def String.Slice.instInhabitedByteIterator.default : ByteIterator

instance String.Slice.instInhabitedByteIterator : Inhabited ByteIterator

def String.Slice.bytes (s : Slice) : Std.Iter UInt8

Creates an iterator over all bytes in {name}s.

Examples:

• {lean}"abc".toSlice.bytes.toList = [97, 98, 99]
• {lean}"ab∀c".toSlice.bytes.toList = [97, 98, 226, 136, 128, 99]

instance String.Slice.ByteIterator.instIteratorUInt8OfPure {m : Type → Type u_1} [Pure m] : Std.Iterator ByteIterator m UInt8

instance String.Slice.ByteIterator.instFiniteUInt8 {m : Type → Type u_1} [Pure m] : Std.Iterators.Finite ByteIterator m

instance String.Slice.ByteIterator.instIteratorLoopUInt8OfMonad {m : Type → Type u_1} {n : Type u_2 → Type u_3} [Monad m] [Monad n] : Std.IteratorLoop ByteIterator m n

structure String.Slice.RevByteIterator : Type

• s : Slice
• offset : Pos.Raw
• hinv : self.offset ≤ self.s.rawEndPos

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

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

Examples:

• {lean}"abc".toSlice.revBytes.toList = [99, 98, 97]
• {lean}"ab∀c".toSlice.revBytes.toList = [99, 128, 136, 226, 98, 97]

instance String.Slice.instInhabitedRevByteIterator : Inhabited RevByteIterator

instance String.Slice.RevByteIterator.instIteratorUInt8OfPure {m : Type → Type u_1} [Pure m] : Std.Iterator RevByteIterator m UInt8

instance String.Slice.RevByteIterator.instFiniteUInt8 {m : Type → Type u_1} [Pure m] : Std.Iterators.Finite RevByteIterator m

instance String.Slice.RevByteIterator.instIteratorLoopUInt8OfMonad {m : Type → Type u_1} {n : Type u_2 → Type u_3} [Monad m] [Monad n] : Std.IteratorLoop RevByteIterator m n

def String.Slice.lines.lineMap (s : Slice) : Slice

def String.Slice.lines (s : Slice) : 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".toSlice.lines.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]

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

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

@[inline]

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

Folds a function over a slice 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".toSlice.foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 2

• "coffee tea and water".toSlice.foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 3

• "coffee tea water".toSlice.foldl (·.push ·) "" = "coffee tea water"

@[inline]

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

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

Examples:

• "coffee tea water".toSlice.foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 2

• "coffee tea and water".toSlice.foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 3

• "coffee tea water".toSlice.foldr (fun c s => s.push c) "" = "retaw aet eeffoc"

@[inline]

def String.Slice.isNat (s : Slice) : Bool

Checks whether the slice 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. Underscores (_) are allowed as digit separators for readability, but cannot appear at the start, at the end, or consecutively.

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

Examples:

• "".toSlice.isNat = false

• "0".toSlice.isNat = true

• "5".toSlice.isNat = true

• "05".toSlice.isNat = true

• "587".toSlice.isNat = true

• "1_000".toSlice.isNat = true

• "100_000_000".toSlice.isNat = true

• "-587".toSlice.isNat = false

• " 5".toSlice.isNat = false

• "2+3".toSlice.isNat = false

• "0xff".toSlice.isNat = false

• "_123".toSlice.isNat = false

• "123_".toSlice.isNat = false

• "12__34".toSlice.isNat = false

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

Interprets a slice 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. Underscores (_) are allowed as digit separators and are ignored during parsing.

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:

• "".toSlice.toNat? = none

• "0".toSlice.toNat? = some 0

• "5".toSlice.toNat? = some 5

• "587".toSlice.toNat? = some 587

• "1_000".toSlice.toNat? = some 1000

• "100_000_000".toSlice.toNat? = some 100000000

• "-587".toSlice.toNat? = none

• " 5".toSlice.toNat? = none

• "2+3".toSlice.toNat? = none

• "0xff".toSlice.toNat? = none

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

Interprets a slice 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. Underscores (_) are allowed as digit separators and are ignored during parsing.

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".toSlice.toNat! = 0

• "5".toSlice.toNat! = 5

• "587".toSlice.toNat! = 587

• "1_000".toSlice.toNat! = 1000

@[inline]

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

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

Examples:

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

• "".toSlice.front? = none

@[inline]

def String.Slice.front (s : Slice) : Char

Returns the first character in s. If s is empty, returns (default : Char).

Examples:

• "abc".toSlice.front = 'a'

• "".toSlice.front = (default : Char)

def String.Slice.isInt (s : Slice) : Bool

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

A slice 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.Slice.toInt? or String.toInt! to convert such a string to an integer.

Examples:

• "".toSlice.isInt = false

• "-".toSlice.isInt = false

• "0".toSlice.isInt = true

• "-0".toSlice.isInt = true

• "5".toSlice.isInt = true

• "587".toSlice.isInt = true

• "-587".toSlice.isInt = true

• "+587".toSlice.isInt = false

• " 5".toSlice.isInt = false

• "2-3".toSlice.isInt = false

• "0xff".toSlice.isInt = false

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

Interprets a slice 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 Slice.isInt to check whether Slice.toInt? would return some. Slice.toInt! is an alternative that panics instead of returning none when the string is not an integer.

Examples:

• "".toSlice.toInt? = none

• "-".toSlice.toInt? = none

• "0".toSlice.toInt? = some 0

• "5".toSlice.toInt? = some 5

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

• "587".toSlice.toInt? = some 587

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

• " 5".toSlice.toInt? = none

• "2-3".toSlice.toInt? = none

• "0xff".toSlice.toInt? = none

@[inline]

def String.Slice.toInt! (s : Slice) : 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 Slice.isInt to check whether Slice.toInt! would return a value. Slice.toInt? is a safer alternative that returns none instead of panicking when the string is not an integer.

Examples:

• "0".toSlice.toInt! = 0

• "5".toSlice.toInt! = 5

• "587".toSlice.toInt! = 587

• "-587".toSlice.toInt! = -587

@[inline]

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

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

Examples:

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

• "".toSlice.back? = none

@[inline]

def String.Slice.back (s : Slice) : Char

Returns the last character in s. If s is empty, returns (default : Char).

Examples:

• "abc".toSlice.back = 'c'

• "".toSlice.back = (default : Char)

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

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

Examples:

• ", ".toSlice.intercalate ["red".toSlice, "green".toSlice, "blue".toSlice] = "red, green, blue"

• " and ".toSlice.intercalate ["tea".toSlice, "coffee".toSlice] = "tea and coffee"

• " | ".toSlice.intercalate ["M".toSlice, "".toSlice, "N".toSlice] = "M | | N"

def String.Slice.toString (s : Slice) : String

Creates a String from a String.Slice by copying the bytes.

instance String.Slice.instToString : ToString Slice

def String.Slice.toName (s : Slice) : Lean.Name

Converts a string to the Lean compiler's representation of names. The resulting name is hierarchical, and the string is split at the dots ('.').

"a.b".toSlice.toName is the name a.b, not «a.b». For the latter, use Name.mkSimple.

instance String.Slice.instToFormat : Std.ToFormat Slice

@[inline]

def Std.Iter.toStringList {α : Type} [Iterator α Id String.Slice] [Iterators.Finite α Id] (i : Iter String.Slice) : List String

Converts a Std.Iter String.Slice to a List String.

def Std.Iter.toStringArray {α : Type} [Iterator α Id String.Slice] [Iterators.Finite α Id] (i : Iter String.Slice) : Array String

Converts a Std.Iter String.Slice to an Array String.