@[simp]

theorem Std.Iterators.Iter.toIterM_empty {β : Type u_1} : (empty β).toIterM = IterM.empty Id β

@[simp]

theorem Std.Iterators.Iter.step_empty {β : Type u_1} : (empty β).step = ⟨IterStep.done, ⋯⟩

@[simp]

theorem Std.Iterators.Iter.toList_empty {β : Type u_1} : (empty β).toList = []

@[simp]

theorem Std.Iterators.Iter.toListRev_empty {β : Type u_1} : (empty β).toListRev = []

@[simp]

theorem Std.Iterators.Iter.toArray_empty {β : Type u_1} : (empty β).toArray = #[]

@[simp]

theorem Std.Iterators.Iter.forIn_empty {m : Type u_1 → Type u_2} {β γ : Type u_1} [Monad m] [LawfulMonad m] {init : γ} {f : β → γ → m (ForInStep γ)} : forIn (empty β) init f = pure init

@[simp]

theorem Std.Iterators.Iter.foldM_empty {m : Type u_1 → Type u_2} {β γ : Type u_1} [Monad m] [LawfulMonad m] {init : γ} {f : γ → β → m γ} : foldM f init (empty β) = pure init

@[simp]

theorem Std.Iterators.Iter.fold_empty {β γ : Type u_1} {init : γ} {f : γ → β → γ} : fold f init (empty β) = init