@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Std.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.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.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.IterM.drain_empty {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [LawfulMonad m] : (empty m β).drain = pure PUnit.unit