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