@[simp]

theorem ReaderT.run_failure {m : Type u_1 → Type u_2} {ρ α : 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} [Monad m] [Alternative m] (x y : ReaderT ρ m α) (ctx : ρ) : (x <|> y).run ctx = (x.run ctx <|> y.run ctx)

@[simp]

theorem StateT.run_failure {m : Type u_1 → Type u_2} {α σ : 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} [Monad m] [Alternative m] (x y : StateT σ m α) (s : σ) : (x <|> y).run s = (x.run s <|> y.run s)