Std.Data.Iterators.Lemmas.Producers.Slice

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

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

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

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

Instances For

source

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

source

@[deprecated Std.Slice.toArray_iter (since := "2025-11-13")]

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

s.toArray = s.iter.toArray

source

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

source

@[deprecated Std.Slice.toList_iter (since := "2025-11-13")]

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

s.toList = s.iter.toList

source

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

source

@[deprecated Std.Slice.toListRev_iter (since := "2025-11-13")]

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

s.toListRev = s.iter.toListRev

source

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

source

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