# Additional theorems on `ForInStep` #

source
@[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)
source
@[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
source
@[simp]
theorem ForInStep.run_done {α✝ : Type u_1} {a : α✝} :
(done a).run = a
source
@[simp]
theorem ForInStep.run_yield {α✝ : Type u_1} {a : α✝} :
(yield a).run = a
source
@[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
source
@[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
source
@[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)
source
@[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
source
@[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
source
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
source
@[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