theorem Std.Slice.Internal.iter_eq_iter {γ : Type u} {α β : Type v} [ToIterator (Slice γ) Id α β] {s : Slice γ} : s.iter = iter s

theorem Std.Slice.iter_eq_toIteratorIter {α β : Type v} {γ : Type u} {s : Slice γ} [ToIterator (Slice γ) Id α β] : s.iter = ToIterator.iter s

theorem Std.Slice.forIn_iter {α : Type v} {γ : Type u} {β : Type v} {m : Type w → Type x} [Monad m] {δ : Type w} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [IteratorLoop α Id m] {s : Slice γ} {init : δ} {f : β → δ → m (ForInStep δ)} : forIn s.iter init f = forIn s init f

theorem Std.Slice.foldlM_iter {γ : Type u} {α β : Type v} {m : Type u_1 → Type u_2} {δ : Type u_1} [Monad m] [ToIterator (Slice γ) Id α β] [Iterator α Id β] [IteratorLoop α Id m] {s : Slice γ} {init : δ} {f : δ → β → m δ} : Iter.foldM f init s.iter = foldlM f init s

theorem Std.Slice.foldl_iter {γ : Type u} {α β : Type v} {δ : Type u_1} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [IteratorLoop α Id Id] {s : Slice γ} {init : δ} {f : δ → β → δ} : Iter.fold f init s.iter = foldl f init s

theorem Std.Slice.size_eq_length_iter {γ : Type u} {α β : Type v} [ToIterator (Slice γ) Id α β] [Iterator α Id β] {s : Slice γ} [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] [SliceSize γ] [LawfulSliceSize γ] : s.size = s.iter.length

@[deprecated Std.Slice.size_eq_length_iter (since := "2026-01-28")]

def Std.Slice.size_eq_count_iter {γ : Type u_1} {α β : Type u_2} [ToIterator (Slice γ) Id α β] [Iterator α Id β] {s : Slice γ} [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] [SliceSize γ] [LawfulSliceSize γ] : s.size = s.iter.length

Equations

• @Std.Slice.size_eq_count_iter = @Std.Slice.size_eq_length_iter

theorem Std.Slice.length_iter_eq_size {γ : Type u} {α β : Type v} [ToIterator (Slice γ) Id α β] [Iterator α Id β] {s : Slice γ} [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] [SliceSize γ] [LawfulSliceSize γ] : s.iter.length = s.size

@[deprecated Std.Slice.length_iter_eq_size (since := "2026-01-28")]

def Std.Slice.count_iter_eq_size {γ : Type u_1} {α β : Type u_2} [ToIterator (Slice γ) Id α β] [Iterator α Id β] {s : Slice γ} [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] [SliceSize γ] [LawfulSliceSize γ] : s.iter.length = s.size

Equations

• @Std.Slice.count_iter_eq_size = @Std.Slice.length_iter_eq_size

@[simp]

theorem Std.Slice.toArray_iter {γ : Type u} {α β : Type v} {s : Slice γ} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [Iterators.Finite α Id] : s.iter.toArray = s.toArray

@[simp]

theorem Std.Slice.toList_iter {γ : Type u} {α β : Type v} {s : Slice γ} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [Iterators.Finite α Id] : s.iter.toList = s.toList

@[simp]

theorem Std.Slice.toListRev_iter {γ : Type u} {α β : Type v} {s : Slice γ} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [Iterators.Finite α Id] : s.iter.toListRev = s.toListRev

theorem Std.Slice.fold_iter {γ : Type u} {α β : Type v} {α✝ : Type u_1} {f : α✝ → β → α✝} {init : α✝} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Finite α Id] {s : Slice γ} : Iter.fold f init s.iter = foldl f init s

theorem Std.Slice.foldM_iter {γ : Type u} {α β : Type v} {δ : Type w} {init : δ} {m : Type w → Type w'} [Monad m] [ToIterator (Slice γ) Id α β] [Iterator α Id β] [IteratorLoop α Id m] [Iterators.Finite α Id] {s : Slice γ} {f : δ → β → m δ} : Iter.foldM f init s.iter = foldlM f init s