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