@[simp]
theorem
ReaderT.run_failure
{m : Type u_1 → Type u_2}
{ρ : Type u_1}
{α : Type u_1}
[Monad m]
[Alternative m]
(ctx : ρ)
:
ReaderT.run failure ctx = failure
@[simp]
theorem
ReaderT.run_orElse
{m : Type u_1 → Type u_2}
{ρ : Type u_1}
{α : Type u_1}
[Monad m]
[Alternative m]
(x : ReaderT ρ m α)
(y : ReaderT ρ m α)
(ctx : ρ)
:
ReaderT.run (HOrElse.hOrElse x fun (x : Unit) => y) ctx = HOrElse.hOrElse (ReaderT.run x ctx) fun (x : Unit) => ReaderT.run y ctx
@[simp]
theorem
StateT.run_failure
{m : Type u_1 → Type u_2}
{α : Type u_1}
{σ : Type u_1}
[Monad m]
[Alternative m]
(s : σ)
:
StateT.run failure s = failure
@[simp]
theorem
StateT.run_orElse
{m : Type u_1 → Type u_2}
{α : Type u_1}
{σ : Type u_1}
[Monad m]
[Alternative m]
(x : StateT σ m α)
(y : StateT σ m α)
(s : σ)
:
StateT.run (HOrElse.hOrElse x fun (x : Unit) => y) s = HOrElse.hOrElse (StateT.run x s) fun (x : Unit) => StateT.run y s