Documentation

Std.Control.ForInStep.Lemmas

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 α)) :
@[simp]
theorem ForInStep.bind_yield {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (a : α) (f : αm (ForInStep α)) :
@[simp]
theorem ForInStep.run_done :
∀ {α : Type u_1} {a : α}, ForInStep.run (ForInStep.done a) = a
@[simp]
theorem ForInStep.run_yield :
∀ {α : Type u_1} {a : α}, ForInStep.run (ForInStep.yield a) = 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 β) :
@[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 α) :
ForInStep.bindList f (a :: l) s = ForInStep.bind s fun b => do let x ← f a b ForInStep.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 α) :
@[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 α) :
@[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 ← ForInStep.bind s f ForInStep.bindList g l x) = ForInStep.bind s fun b => do let x ← f b ForInStep.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 α) :
ForInStep.bindList f (a :: l) s = do let x ← ForInStep.bind s (f a) ForInStep.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₁ : List α) (l₂ : List α) :
ForInStep.bindList f (l₁ ++ l₂) s = do let x ← ForInStep.bindList f l₁ s ForInStep.bindList f l₂ x