Documentation

Batteries.Control.Lemmas

theorem ReaderT.ext_iff {ρ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x : ReaderT ρ m α} {y : ReaderT ρ m α} :
x = y ∀ (ctx : ρ), x.run ctx = y.run ctx
@[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
theorem StateT.ext_iff {σ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x : StateT σ m α} {y : StateT σ m α} :
x = y ∀ (s : σ), x.run s = y.run s
@[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