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