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

• currPos : s.Pos

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

@[implicit_reducible]

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

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

Creates an iterator over the valid positions within s, starting at p.

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]

@[implicit_reducible]

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

@[implicit_reducible]

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.length` 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

@[implicit_reducible]

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

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

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

Creates an iterator over all valid positions within s that are strictly smaller than p, starting from the position before p and iterating towards the first one.

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]

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance String.Slice.instInhabitedByteIterator : Inhabited ByteIterator

def String.Slice.instInhabitedByteIterator.default : 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]

@[implicit_reducible]

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

@[implicit_reducible]

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]

@[implicit_reducible]

instance String.Slice.instInhabitedRevByteIterator : Inhabited RevByteIterator

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance String.Slice.RevByteIterator.instForInCharOfMonad {m : Type u → Type v} [Monad m] : ForIn m Slice Char

@[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.Internal.ofToSliceWithProof {s : String} : { p : s.toSlice.Pos // p ≠ s.toSlice.endPos } → { p : s.Pos // p ≠ s.endPos }

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

Creates an iterator over the valid positions within s, starting at 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]

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

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

Creates an iterator over all valid positions within s that are strictly smaller than p, starting from the position before p and iterating towards the first one.

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

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

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

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

@[implicit_reducible]

instance String.instForInCharOfMonad {m : Type u → Type v} [Monad m] : ForIn m String Char