# Documentation

Std.Control.ForInStep.Lemmas

# Additional theorems on ForInStep#

@[simp]
theorem ForInStep.bind_done {m : Type u_1 → Type u_2} {α : Type u_1} [] (a : α) (f : αm ()) :
=
@[simp]
theorem ForInStep.bind_yield {m : Type u_1 → Type u_2} {α : Type u_1} [] (a : α) (f : αm ()) :
= f a
@[simp]
theorem ForInStep.run_done :
∀ {α : Type u_1} {a : α},
@[simp]
theorem ForInStep.run_yield :
∀ {α : Type u_1} {a : α},
@[simp]
theorem ForInStep.bindList_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (f : αβm ()) (s : ) :
= pure s
@[simp]
theorem ForInStep.bindList_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (f : αβm ()) (s : ) (a : α) (l : List α) :
ForInStep.bindList f (a :: l) s = ForInStep.bind s fun b => do let x ← f a b
@[simp]
theorem ForInStep.done_bindList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (f : αβm ()) (a : β) (l : List α) :
=
@[simp]
theorem ForInStep.bind_yield_bindList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (f : αβm ()) (s : ) (l : List α) :
(ForInStep.bind s fun a => ) =
@[simp]
theorem ForInStep.bind_bindList_assoc {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [] [] (f : βm ()) (g : αβm ()) (s : ) (l : List α) :
(do let x ← ) = ForInStep.bind s fun b => do let x ← f b
theorem ForInStep.bindList_cons' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] [] (f : αβm ()) (s : ) (a : α) (l : List α) :
ForInStep.bindList f (a :: l) s = do let x ← ForInStep.bind s (f a)
@[simp]
theorem ForInStep.bindList_append {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] [] (f : αβm ()) (s : ) (l₁ : List α) (l₂ : List α) :
ForInStep.bindList f (l₁ ++ l₂) s = do let x ←