@[simp]

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

@[simp]

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

theorem Std.Slice.Internal.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 (iter s) = foldlM f init s

theorem Std.Slice.foldlM_toList {γ : Type u} {α β : Type v} {m : Type u_1 → Type u_2} {δ : Type u_1} [Monad m] [ToIterator (Slice γ) Id α β] [Iterator α Id β] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] [Iterators.Finite α Id] [LawfulMonad m] {s : Slice γ} {init : δ} {f : δ → β → m δ} : List.foldlM f init s.toList = foldlM f init s

theorem Std.Slice.foldlM_toArray {γ : Type u} {α β : Type v} {m : Type u_1 → Type u_2} {δ : Type u_1} [Monad m] [ToIterator (Slice γ) Id α β] [Iterator α Id β] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] [Iterators.Finite α Id] [LawfulMonad m] {s : Slice γ} {init : δ} {f : δ → β → m δ} : Array.foldlM f init s.toArray = foldlM f init s

theorem Std.Slice.Internal.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 (iter s) = foldl f init s

theorem Std.Slice.foldl_toList {γ : Type u} {α β : Type v} {δ : Type u_1} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] [Iterators.Finite α Id] {s : Slice γ} {init : δ} {f : δ → β → δ} : List.foldl f init s.toList = foldl f init s

theorem Std.Slice.foldl_toArray {γ : Type u} {α β : Type v} {δ : Type u_1} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] [Iterators.Finite α Id] {s : Slice γ} {init : δ} {f : δ → β → δ} : Array.foldl f init s.toArray = foldl f init s

@[simp]

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

@[simp]

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

@[simp]

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