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

• currPos : s.Pos

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

Equations

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

@[instance_reducible]

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

Equations

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

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.

Equations

• String.Slice.positionsFrom p = { internalState := { currPos := 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]

Equations

• s.positions = String.Slice.positionsFrom s.startPos

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

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_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

Equations

• String.Slice.PosIterator.instIteratorLoopSubtypePosNeEndPosOfMonad = Std.IteratorLoop.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.Iter.map (fun (x : { p : s.Pos // p ≠ s.endPos }) => match x with | ⟨pos, h⟩ => pos.get h) s.positions

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

Equations

• s.length = s.positions.length

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

• currPos : s.Pos

@[instance_reducible]

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

Equations

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

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

Equations

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

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.

Equations

• s.revPositionsFrom p = { internalState := { currPos := p } }

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 = s.revPositionsFrom s.endPos

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

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_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

Equations

• String.Slice.RevPosIterator.instIteratorLoopSubtypePosNeEndPosOfMonad = Std.IteratorLoop.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.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

@[instance_reducible]

instance String.Slice.instInhabitedByteIterator : Inhabited ByteIterator

Equations

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

def String.Slice.instInhabitedByteIterator.default : ByteIterator

Equations

• String.Slice.instInhabitedByteIterator.default = { s := default, offset := 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_reducible]

instance String.Slice.ByteIterator.instIteratorUInt8OfPure {m : Type → Type u_1} [Pure m] : Std.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_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

Equations

• String.Slice.ByteIterator.instIteratorLoopUInt8OfMonad = Std.IteratorLoop.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_reducible]

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_reducible]

instance String.Slice.RevByteIterator.instIteratorUInt8OfPure {m : Type → Type u_1} [Pure m] : Std.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_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

Equations

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

@[instance_reducible]

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

Equations

• String.Slice.RevByteIterator.instForInCharOfMonad = { forIn := fun {β : Type ?u.25} (s : String.Slice) (b : β) (f : Char → β → m (ForInStep β)) => forIn s.chars b f }

@[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.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.Iter.fold (flip f) init s.revChars

@[inline]

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

Equations

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

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.

Equations

• s.positionsFrom p = Std.Iter.map String.Internal.ofToSliceWithProof (String.Slice.positionsFrom p.toSlice)

@[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 = s.positionsFrom s.startPos

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

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.

Equations

• s.revPositionsFrom p = Std.Iter.map String.Internal.ofToSliceWithProof (s.toSlice.revPositionsFrom p.toSlice)

@[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 = s.revPositionsFrom s.endPos

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

@[instance_reducible]

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

Equations

• String.instForInCharOfMonad = { forIn := fun {β : Type ?u.19} (s : String) (b : β) (f : Char → β → m (ForInStep β)) => forIn s.toSlice b f }