@[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 ReaderT.run_throw {ε : Type u_1} {m : Type u_2 → Type u_3} {ρ α : Type u_2} [MonadExceptOf ε m] (e : ε) (ctx : ρ) : (throw e).run ctx = throw e

@[simp]

theorem ReaderT.run_throwThe {ε : Type u_1} {m : Type u_2 → Type u_3} {ρ α : Type u_2} [MonadExceptOf ε m] (e : ε) (ctx : ρ) : (throwThe ε e).run ctx = throwThe ε e

@[simp]

theorem ReaderT.run_tryCatch {ε : Type u_1} {m : Type u_2 → Type u_3} {ρ α : Type u_2} [MonadExceptOf ε m] (body : ReaderT ρ m α) (handler : ε → ReaderT ρ m α) (ctx : ρ) : (tryCatch body handler).run ctx = tryCatch (body.run ctx) fun (x : ε) => (handler x).run ctx

@[simp]

theorem ReaderT.run_tryCatchThe {ε : Type u_1} {m : Type u_2 → Type u_3} {ρ α : Type u_2} [MonadExceptOf ε m] (body : ReaderT ρ m α) (handler : ε → ReaderT ρ m α) (ctx : ρ) : (tryCatchThe ε body handler).run ctx = tryCatchThe ε (body.run ctx) fun (x : ε) => (handler x).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)

@[simp]

theorem StateT.run_throw {m : Type u_1 → Type u_2} {ε : Type u_3} {σ α : Type u_1} [Monad m] [MonadExceptOf ε m] (e : ε) (s : σ) : (throw e).run s = do let a ← throw e pure (a, s)

@[simp]

theorem StateT.run_throwThe {m : Type u_1 → Type u_2} {ε : Type u_3} {σ α : Type u_1} [Monad m] [MonadExceptOf ε m] (e : ε) (s : σ) : (throwThe ε e).run s = do let a ← throwThe ε e pure (a, s)

@[simp]

theorem StateT.run_tryCatch {m : Type u_1 → Type u_2} {ε : Type u_3} {σ α : Type u_1} [Monad m] [MonadExceptOf ε m] (body : StateT σ m α) (handler : ε → StateT σ m α) (s : σ) : (tryCatch body handler).run s = tryCatch (body.run s) fun (x : ε) => (handler x).run s

@[simp]

theorem StateT.run_tryCatchThe {m : Type u_1 → Type u_2} {ε : Type u_3} {σ α : Type u_1} [Monad m] [MonadExceptOf ε m] (body : StateT σ m α) (handler : ε → StateT σ m α) (s : σ) : (tryCatchThe ε body handler).run s = tryCatchThe ε (body.run s) fun (x : ε) => (handler x).run s