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

Equations

• s.isEmpty = (s.utf8ByteSize == 0)

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

Equations

• One or more equations did not get rendered due to their size.

instance String.Slice.instBEq : BEq Slice

Equations

• String.Slice.instBEq = { beq := String.Slice.beq }

@[extern lean_slice_hash]

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

instance String.Slice.instHashable : Hashable Slice

Equations

• String.Slice.instHashable = { hash := String.Slice.hash }

instance String.Slice.instLT : LT Slice

Equations

• String.Slice.instLT = { lt := fun (x y : String.Slice) => x.copy < y.copy }

@[extern lean_slice_dec_lt]

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

Equations

• x.instDecidableLt y = inferInstanceAs (Decidable (x.copy < y.copy))

instance String.Slice.instOrd : Ord Slice

Equations

• String.Slice.instOrd = { compare := fun (x y : String.Slice) => compareOfLessAndBEq x y }

instance String.Slice.instLE : LE Slice

Equations

• String.Slice.instLE = { le := fun (x y : String.Slice) => ¬x < y }

instance String.Slice.instDecidableLE : DecidableLE Slice

Equations

• x.instDecidableLE y = inferInstanceAs (Decidable ¬x < y)

@[inline]

def String.Slice.startsWith {ρ : Type} [Pattern.ForwardPattern ρ] (s : Slice) (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

Equations

• s.startsWith pat = String.Slice.Pattern.ForwardPattern.startsWith s pat

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

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

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

Equations

• String.Slice.instInhabitedSplitIterator = { default := String.Slice.instInhabitedSplitIterator.default }

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

Equations

• String.Slice.instInhabitedSplitIterator.default = String.Slice.SplitIterator.atEnd

instance String.Slice.SplitIterator.instIteratorOfPure {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Pattern.ToForwardSearcher ρ σ] {m : Type → Type u_1} [Pure m] : Std.Iterators.Iterator (SplitIterator ρ) m Slice

Equations

• One or more equations did not get rendered due to their size.

instance String.Slice.SplitIterator.instIteratorCollectOfMonad {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Pattern.ToForwardSearcher ρ σ] {m : Type → Type u_1} {n : Type → Type u_2} [Monad m] [Monad n] : Std.Iterators.IteratorCollect (SplitIterator ρ) m n

Equations

• String.Slice.SplitIterator.instIteratorCollectOfMonad = Std.Iterators.IteratorCollect.defaultImplementation

instance String.Slice.SplitIterator.instIteratorCollectPartialOfMonad {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Pattern.ToForwardSearcher ρ σ] {m : Type → Type u_1} {n : Type → Type u_2} [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial (SplitIterator ρ) m n

Equations

• String.Slice.SplitIterator.instIteratorCollectPartialOfMonad = Std.Iterators.IteratorCollectPartial.defaultImplementation

instance String.Slice.SplitIterator.instIteratorLoopOfMonad {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Pattern.ToForwardSearcher ρ σ] {m : Type → Type u_1} {n : Type u_2 → Type u_3} [Monad m] [Monad n] : Std.Iterators.IteratorLoop (SplitIterator ρ) m n

Equations

• String.Slice.SplitIterator.instIteratorLoopOfMonad = Std.Iterators.IteratorLoop.defaultImplementation

instance String.Slice.SplitIterator.instIteratorLoopPartialOfMonad {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Pattern.ToForwardSearcher ρ σ] {m : Type → Type u_1} {n : Type u_2 → Type u_3} [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (SplitIterator ρ) m n

Equations

• String.Slice.SplitIterator.instIteratorLoopPartialOfMonad = Std.Iterators.IteratorLoopPartial.defaultImplementation

@[specialize #[4]]

def String.Slice.split {ρ : Type} {σ : Slice → Type} [Pattern.ToForwardSearcher ρ σ] (s : Slice) (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).allowNontermination.toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]

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

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

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

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

Equations

• s.split pat = { internalState := String.Slice.SplitIterator.operating s s.startPos (String.Slice.Pattern.ToForwardSearcher.toSearcher s pat) }

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

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

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

Equations

• String.Slice.instInhabitedSplitInclusiveIterator.default = String.Slice.SplitInclusiveIterator.atEnd

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

Equations

• String.Slice.instInhabitedSplitInclusiveIterator = { default := String.Slice.instInhabitedSplitInclusiveIterator.default }

instance String.Slice.SplitInclusiveIterator.instIteratorOfPure {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Pattern.ToForwardSearcher ρ σ] {m : Type → Type u_1} [Pure m] : Std.Iterators.Iterator (SplitInclusiveIterator ρ) m Slice

Equations

• One or more equations did not get rendered due to their size.

instance String.Slice.SplitInclusiveIterator.instIteratorCollectOfMonad {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Pattern.ToForwardSearcher ρ σ] {m : Type → Type u_1} {n : Type → Type u_2} [Monad m] [Monad n] : Std.Iterators.IteratorCollect (SplitInclusiveIterator ρ) m n

Equations

• String.Slice.SplitInclusiveIterator.instIteratorCollectOfMonad = Std.Iterators.IteratorCollect.defaultImplementation

instance String.Slice.SplitInclusiveIterator.instIteratorCollectPartialOfMonad {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Pattern.ToForwardSearcher ρ σ] {m : Type → Type u_1} {n : Type → Type u_2} [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial (SplitInclusiveIterator ρ) m n

Equations

• String.Slice.SplitInclusiveIterator.instIteratorCollectPartialOfMonad = Std.Iterators.IteratorCollectPartial.defaultImplementation

instance String.Slice.SplitInclusiveIterator.instIteratorLoopOfMonad {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Pattern.ToForwardSearcher ρ σ] {m : Type → Type u_1} {n : Type u_2 → Type u_3} [Monad m] [Monad n] : Std.Iterators.IteratorLoop (SplitInclusiveIterator ρ) m n

Equations

• String.Slice.SplitInclusiveIterator.instIteratorLoopOfMonad = Std.Iterators.IteratorLoop.defaultImplementation

instance String.Slice.SplitInclusiveIterator.instIteratorLoopPartialOfMonad {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Pattern.ToForwardSearcher ρ σ] {m : Type → Type u_1} {n : Type u_2 → Type u_3} [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (SplitInclusiveIterator ρ) m n

Equations

• String.Slice.SplitInclusiveIterator.instIteratorLoopPartialOfMonad = Std.Iterators.IteratorLoopPartial.defaultImplementation

@[specialize #[4]]

def String.Slice.splitInclusive {ρ : Type} {σ : Slice → Type} [Pattern.ToForwardSearcher ρ σ] (s : Slice) (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).allowNontermination.toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]

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

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

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

Equations

• s.splitInclusive pat = { internalState := String.Slice.SplitInclusiveIterator.operating s s.startPos (String.Slice.Pattern.ToForwardSearcher.toSearcher s pat) }

@[inline]

def String.Slice.dropPrefix? {ρ : Type} [Pattern.ForwardPattern ρ] (s : Slice) (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

Equations

• s.dropPrefix? pat = Option.map s.replaceStart (String.Slice.Pattern.ForwardPattern.dropPrefix? s pat)

@[specialize #[3]]

def String.Slice.dropPrefix {ρ : Type} [Pattern.ForwardPattern ρ] (s : Slice) (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

Equations

• s.dropPrefix pat = (s.dropPrefix? pat).getD s

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

Equations

• s.drop n = s.replaceStart (s.startPos.nextn n)

@[inline]

def String.Slice.dropWhile {ρ : Type} [Pattern.ForwardPattern ρ] (s : Slice) (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

Equations

• s.dropWhile pat = String.Slice.dropWhile.go✝ pat s

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

Equations

• s.trimAsciiStart = s.dropWhile Char.isWhitespace

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

Equations

• s.take n = s.replaceEnd (s.startPos.nextn n)

@[inline]

def String.Slice.takeWhile {ρ : Type} [Pattern.ForwardPattern ρ] (s : Slice) (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

Equations

• s.takeWhile pat = String.Slice.takeWhile.go✝ s pat s.startPos

@[specialize #[6]]

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

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

Equations

• s.find? pat = match String.Slice.Pattern.Internal.nextMatch (String.Slice.Pattern.ToForwardSearcher.toSearcher s pat) with | some (fst, startPos, snd) => some startPos | none => none

@[specialize #[6]]

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

Equations

• s.contains pat = (String.Slice.Pattern.Internal.nextMatch (String.Slice.Pattern.ToForwardSearcher.toSearcher s pat)).isSome

@[inline]

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

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

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

Equations

• s.all pat = (s.dropWhile pat).isEmpty

@[inline]

def String.Slice.endsWith {ρ : Type} [Pattern.BackwardPattern ρ] (s : Slice) (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

Equations

• s.endsWith pat = String.Slice.Pattern.BackwardPattern.endsWith s pat

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

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

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

Equations

• String.Slice.instInhabitedRevSplitIterator = { default := String.Slice.instInhabitedRevSplitIterator.default }

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

Equations

• String.Slice.instInhabitedRevSplitIterator.default = String.Slice.RevSplitIterator.atEnd

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

Equations

• One or more equations did not get rendered due to their size.

instance String.Slice.RevSplitIterator.instIteratorCollectOfMonad {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Pattern.ToBackwardSearcher ρ σ] {m : Type → Type u_1} {n : Type → Type u_2} [Monad m] [Monad n] : Std.Iterators.IteratorCollect (RevSplitIterator ρ) m n

Equations

• String.Slice.RevSplitIterator.instIteratorCollectOfMonad = Std.Iterators.IteratorCollect.defaultImplementation

instance String.Slice.RevSplitIterator.instIteratorCollectPartialOfMonad {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Pattern.ToBackwardSearcher ρ σ] {m : Type → Type u_1} {n : Type → Type u_2} [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial (RevSplitIterator ρ) m n

Equations

• String.Slice.RevSplitIterator.instIteratorCollectPartialOfMonad = Std.Iterators.IteratorCollectPartial.defaultImplementation

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

Equations

• String.Slice.RevSplitIterator.instIteratorLoopOfMonad = Std.Iterators.IteratorLoop.defaultImplementation

instance String.Slice.RevSplitIterator.instIteratorLoopPartialOfMonad {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [Pattern.ToBackwardSearcher ρ σ] {m : Type → Type u_1} {n : Type u_2 → Type u_3} [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RevSplitIterator ρ) m n

Equations

• String.Slice.RevSplitIterator.instIteratorLoopPartialOfMonad = Std.Iterators.IteratorLoopPartial.defaultImplementation

@[specialize #[4]]

def String.Slice.revSplit {σ : Slice → Type} {ρ : Type} [Pattern.ToBackwardSearcher ρ σ] (s : Slice) (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).allowNontermination.toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]

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

Equations

• s.revSplit pat = { internalState := String.Slice.RevSplitIterator.operating s s.endPos (String.Slice.Pattern.ToBackwardSearcher.toSearcher s pat) }

@[inline]

def String.Slice.dropSuffix? {ρ : Type} [Pattern.BackwardPattern ρ] (s : Slice) (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

Equations

• s.dropSuffix? pat = Option.map s.replaceEnd (String.Slice.Pattern.BackwardPattern.dropSuffix? s pat)

@[specialize #[3]]

def String.Slice.dropSuffix {ρ : Type} [Pattern.BackwardPattern ρ] (s : Slice) (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

Equations

• s.dropSuffix pat = (s.dropSuffix? pat).getD s

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

Equations

• s.dropEnd n = s.replaceEnd (s.endPos.prevn n)

@[inline]

def String.Slice.dropEndWhile {ρ : Type} [Pattern.BackwardPattern ρ] (s : Slice) (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

Equations

• s.dropEndWhile pat = String.Slice.dropEndWhile.go✝ pat s

@[inline]

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

Removes trailing 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.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

Equations

• s.trimAsciiEnd = s.dropEndWhile Char.isWhitespace

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

Equations

• s.takeEnd n = s.replaceStart (s.endPos.prevn n)

@[inline]

def String.Slice.takeEndWhile {ρ : Type} [Pattern.BackwardPattern ρ] (s : Slice) (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

Equations

• s.takeEndWhile pat = String.Slice.takeEndWhile.go✝ s pat s.endPos

@[specialize #[6]]

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

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

Equations

• s.revFind? pat = match String.Slice.Pattern.Internal.nextMatch (String.Slice.Pattern.ToBackwardSearcher.toSearcher s pat) with | some (fst, startPos, snd) => some startPos | none => 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

Equations

• s.trimAscii = s.trimAsciiStart.trimAsciiEnd

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

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

Equations

• s1.eqIgnoreAsciiCase s2 = (s1.utf8ByteSize == s2.utf8ByteSize && String.Slice.eqIgnoreAsciiCase.go✝ s1 s1.startPos.offset s2 s2.startPos.offset)

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

• currPos : s.Pos

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

Equations

• String.Slice.instInhabitedPosIterator = { default := String.Slice.instInhabitedPosIterator.default }

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

Equations

• String.Slice.instInhabitedPosIterator.default = { currPos := default }

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]

Equations

• s.positions = { internalState := { currPos := s.startPos } }

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

Equations

• One or more equations did not get rendered due to their size.

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

instance String.Slice.PosIterator.instIteratorCollectSubtypePosNeEndPosOfMonad {m : Type → Type u_1} {n : Type → Type u_2} {s : Slice} [Monad m] [Monad n] : Std.Iterators.IteratorCollect s.PosIterator m n

Equations

• String.Slice.PosIterator.instIteratorCollectSubtypePosNeEndPosOfMonad = Std.Iterators.IteratorCollect.defaultImplementation

instance String.Slice.PosIterator.instIteratorCollectPartialSubtypePosNeEndPosOfMonad {m : Type → Type u_1} {n : Type → Type u_2} {s : Slice} [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial s.PosIterator m n

Equations

• String.Slice.PosIterator.instIteratorCollectPartialSubtypePosNeEndPosOfMonad = Std.Iterators.IteratorCollectPartial.defaultImplementation

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

Equations

• String.Slice.PosIterator.instIteratorLoopSubtypePosNeEndPosOfMonad = Std.Iterators.IteratorLoop.defaultImplementation

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

Equations

• String.Slice.PosIterator.instIteratorLoopPartialSubtypePosNeEndPosOfMonad = Std.Iterators.IteratorLoopPartial.defaultImplementation

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

Equations

• s.chars = Std.Iterators.Iter.map (fun (x : { p : s.Pos // p ≠ s.endPos }) => match x with | ⟨pos, h⟩ => pos.get h) s.positions

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

• currPos : s.Pos

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

Equations

• String.Slice.instInhabitedRevPosIterator.default = { currPos := default }

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

Equations

• String.Slice.instInhabitedRevPosIterator = { default := String.Slice.instInhabitedRevPosIterator.default }

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]

Equations

• s.revPositions = { internalState := { currPos := s.endPos } }

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

Equations

• One or more equations did not get rendered due to their size.

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

instance String.Slice.RevPosIterator.instIteratorCollectSubtypePosNeEndPosOfMonad {m : Type → Type u_1} {n : Type → Type u_2} {s : Slice} [Monad m] [Monad n] : Std.Iterators.IteratorCollect s.RevPosIterator m n

Equations

• String.Slice.RevPosIterator.instIteratorCollectSubtypePosNeEndPosOfMonad = Std.Iterators.IteratorCollect.defaultImplementation

instance String.Slice.RevPosIterator.instIteratorCollectPartialSubtypePosNeEndPosOfMonad {m : Type → Type u_1} {n : Type → Type u_2} {s : Slice} [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial s.RevPosIterator m n

Equations

• String.Slice.RevPosIterator.instIteratorCollectPartialSubtypePosNeEndPosOfMonad = Std.Iterators.IteratorCollectPartial.defaultImplementation

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

Equations

• String.Slice.RevPosIterator.instIteratorLoopSubtypePosNeEndPosOfMonad = Std.Iterators.IteratorLoop.defaultImplementation

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

Equations

• String.Slice.RevPosIterator.instIteratorLoopPartialSubtypePosNeEndPosOfMonad = Std.Iterators.IteratorLoopPartial.defaultImplementation

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

Equations

• s.revChars = Std.Iterators.Iter.map (fun (x : { p : s.Pos // p ≠ s.endPos }) => match x with | ⟨pos, h⟩ => pos.get h) s.revPositions

structure String.Slice.ByteIterator : Type

• s : Slice
• offset : Pos.Raw

def String.Slice.instInhabitedByteIterator.default : ByteIterator

Equations

• String.Slice.instInhabitedByteIterator.default = { s := default, offset := default }

instance String.Slice.instInhabitedByteIterator : Inhabited ByteIterator

Equations

• String.Slice.instInhabitedByteIterator = { default := String.Slice.instInhabitedByteIterator.default }

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]

Equations

• s.bytes = { internalState := { s := s, offset := s.startPos.offset } }

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

Equations

• One or more equations did not get rendered due to their size.

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

instance String.Slice.ByteIterator.instIteratorCollectUInt8OfMonad {m : Type → Type u_1} {n : Type → Type u_2} [Monad m] [Monad n] : Std.Iterators.IteratorCollect ByteIterator m n

Equations

• String.Slice.ByteIterator.instIteratorCollectUInt8OfMonad = Std.Iterators.IteratorCollect.defaultImplementation

instance String.Slice.ByteIterator.instIteratorCollectPartialUInt8OfMonad {m : Type → Type u_1} {n : Type → Type u_2} [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial ByteIterator m n

Equations

• String.Slice.ByteIterator.instIteratorCollectPartialUInt8OfMonad = Std.Iterators.IteratorCollectPartial.defaultImplementation

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

Equations

• String.Slice.ByteIterator.instIteratorLoopUInt8OfMonad = Std.Iterators.IteratorLoop.defaultImplementation

instance String.Slice.ByteIterator.instIteratorLoopPartialUInt8OfMonad {m : Type → Type u_1} {n : Type u_2 → Type u_3} [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial ByteIterator m n

Equations

• String.Slice.ByteIterator.instIteratorLoopPartialUInt8OfMonad = Std.Iterators.IteratorLoopPartial.defaultImplementation

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]

Equations

• s.revBytes = { internalState := { s := s, offset := s.endPos.offset, hinv := ⋯ } }

instance String.Slice.instInhabitedRevByteIterator : Inhabited RevByteIterator

Equations

• String.Slice.instInhabitedRevByteIterator = { default := let s := default; { s := s, offset := s.endPos.offset, hinv := String.Slice.instInhabitedRevByteIterator._proof_1 } }

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

Equations

• One or more equations did not get rendered due to their size.

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

instance String.Slice.RevByteIterator.instIteratorCollectUInt8OfMonad {m : Type → Type u_1} {n : Type → Type u_2} [Monad m] [Monad n] : Std.Iterators.IteratorCollect RevByteIterator m n

Equations

• String.Slice.RevByteIterator.instIteratorCollectUInt8OfMonad = Std.Iterators.IteratorCollect.defaultImplementation

instance String.Slice.RevByteIterator.instIteratorCollectPartialUInt8OfMonad {m : Type → Type u_1} {n : Type → Type u_2} [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial RevByteIterator m n

Equations

• String.Slice.RevByteIterator.instIteratorCollectPartialUInt8OfMonad = Std.Iterators.IteratorCollectPartial.defaultImplementation

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

Equations

• String.Slice.RevByteIterator.instIteratorLoopUInt8OfMonad = Std.Iterators.IteratorLoop.defaultImplementation

instance String.Slice.RevByteIterator.instIteratorLoopPartialUInt8OfMonad {m : Type → Type u_1} {n : Type u_2 → Type u_3} [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial RevByteIterator m n

Equations

• String.Slice.RevByteIterator.instIteratorLoopPartialUInt8OfMonad = Std.Iterators.IteratorLoopPartial.defaultImplementation

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

Equations

• String.Slice.lines.lineMap s = match s.dropSuffix? '\n' with | some s => match s.dropSuffix? '\x0d' with | some s => s | x => s | x => s

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.allowNontermination.toList == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]

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

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

Equations

• s.lines = Std.Iterators.Iter.map String.Slice.lines.lineMap (s.splitInclusive '\n')

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

Equations

• String.Slice.foldl f init s = Std.Iterators.Iter.fold f init s.chars

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

Equations

• String.Slice.foldr f init s = Std.Iterators.Iter.fold (flip f) init s.revChars

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

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

• "-587".toSlice.isNat = false

• " 5".toSlice.isNat = false

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

• "0xff".toSlice.isNat = false

Equations

• s.isNat = (!s.isEmpty && s.all Char.isDigit)

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.

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

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

• " 5".toSlice.toNat? = none

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

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

Equations

• s.toNat? = if s.isNat = true then some (String.Slice.foldl (fun (n : Nat) (c : Char) => n * 10 + (c.toNat - '0'.toNat)) 0 s) else 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.

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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

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

Examples:

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

• "".toSlice.front? = none

Equations

• s.front? = s.startPos.get?

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

Equations

• s.front = s.front?.getD default

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

Equations

• s.back? = s.endPos.prev?.bind fun (x : s.Pos) => x.get?

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

Equations

• s.back = s.back?.getD default