Additional theorems on ForInStep

@[simp]

theorem ForInStep.bind_done {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (a : α) (f : α → m (ForInStep α)) : (done a).bind f = pure (done a)

@[simp]

theorem ForInStep.bind_yield {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (a : α) (f : α → m (ForInStep α)) : (yield a).bind f = f a

@[simp]

theorem ForInStep.run_done {α✝ : Type u_1} {a : α✝} : (done a).run = a

@[simp]

theorem ForInStep.run_yield {α✝ : Type u_1} {a : α✝} : (yield a).run = a

@[simp]

theorem ForInStep.bindList_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m (ForInStep β)) (s : ForInStep β) : bindList f [] s = pure s

@[simp]

theorem ForInStep.bindList_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m (ForInStep β)) (s : ForInStep β) (a : α) (l : List α) : bindList f (a :: l) s = s.bind fun (b : β) => do let x ← f a b bindList f l x

@[simp]

theorem ForInStep.done_bindList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m (ForInStep β)) (a : β) (l : List α) : bindList f l (done a) = pure (done a)

@[simp]

theorem ForInStep.bind_yield_bindList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m (ForInStep β)) (s : ForInStep β) (l : List α) : (s.bind fun (a : β) => bindList f l (yield a)) = bindList f l s

@[simp]

theorem ForInStep.bind_bindList_assoc {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] [LawfulMonad m] (f : β → m (ForInStep β)) (g : α → β → m (ForInStep β)) (s : ForInStep β) (l : List α) : (do let x ← s.bind f bindList g l x) = s.bind fun (b : β) => do let x ← f b bindList g l x

theorem ForInStep.bindList_cons' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → β → m (ForInStep β)) (s : ForInStep β) (a : α) (l : List α) : bindList f (a :: l) s = do let x ← s.bind (f a) bindList f l x

@[simp]

theorem ForInStep.bindList_append {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → β → m (ForInStep β)) (s : ForInStep β) (l₁ l₂ : List α) : bindList f (l₁ ++ l₂) s = do let x ← bindList f l₁ s bindList f l₂ x