@[simp]

theorem Std.Iterators.IterM.step_empty {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] : (empty m β).step = pure ⟨IterStep.done, ⋯⟩

@[simp]

theorem Std.Iterators.IterM.toList_empty {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [LawfulMonad m] : (empty m β).toList = pure []

@[simp]

theorem Std.Iterators.IterM.toListRev_empty {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [LawfulMonad m] : (empty m β).toListRev = pure []

@[simp]

theorem Std.Iterators.IterM.toArray_empty {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [LawfulMonad m] : (empty m β).toArray = pure #[]

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Std.Iterators.IterM.drain_empty {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [LawfulMonad m] : (empty m β).drain = pure PUnit.unit