Documentation

Batteries.Control.Lemmas

@[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