Lemmas about StateT

@[implicit_reducible]

instance StateT.instMonadLift_toMathlib {m : Type u → Type v} {m' : Type u → Type w} {σ : Type u} [MonadLift m m'] : MonadLift (StateT σ m) (StateT σ m')

@[simp]

theorem StateT.liftM_of_liftM_eq {m : Type u → Type v} {m' : Type u → Type w} {σ α : Type u} [MonadLift m m'] (x : StateT σ m α) : liftM x = mk fun (s : σ) => liftM (x.run s)

theorem StateT.liftM_def {m : Type u → Type v} {σ α : Type u} [Monad m] (x : m α) : liftM x = StateT.lift x

@[simp]

theorem StateT.run_liftM {m : Type u → Type v} {σ α : Type u} [Monad m] (x : m α) (s : σ) : (liftM x).run s = do let a ← x pure (a, s)

theorem StateT.monad_pure_def {m : Type u → Type v} {σ α : Type u} [Monad m] (x : α) : pure x = StateT.pure x

theorem StateT.monad_bind_def {m : Type u → Type v} {σ α β : Type u} [Monad m] (x : StateT σ m α) (f : α → StateT σ m β) : x >>= f = x.bind f

theorem StateT.monad_failure_eq {m : Type u → Type v} {σ α : Type u} [Monad m] [Alternative m] : failure = StateT.failure

@[simp]

theorem StateT.run_failure' {m : Type u → Type v} {σ α : Type u} [Monad m] [Alternative m] : failure.run = fun (x : σ) => failure

@[simp]

theorem StateT.mk_pure_eq_pure {m : Type u → Type v} {σ α : Type u} [Monad m] (x : α) : (mk fun (s : σ) => pure (x, s)) = pure x

StateT.run' lemmas

@[simp]

theorem StateT.run'_pure' {m : Type u → Type v} {σ α : Type u} [Monad m] [LawfulMonad m] (x : α) (s : σ) : (pure x).run' s = pure x

@[simp]

theorem StateT.run'_bind' {m : Type u → Type v} {σ α β : Type u} [Monad m] [LawfulMonad m] (x : StateT σ m α) (f : α → StateT σ m β) (s : σ) : (x >>= f).run' s = do let x ← x.run s match x with | (a, s') => (f a).run' s'

@[simp]

theorem StateT.run'_map' {m : Type u → Type v} {σ α β : Type u} [Monad m] [LawfulMonad m] (x : StateT σ m α) (f : α → β) (s : σ) : (f <$> x).run' s = f <$> x.run' s

@[simp]

theorem StateT.run'_lift' {m : Type u → Type v} {σ α : Type u} [Monad m] [LawfulMonad m] (x : m α) (s : σ) : (StateT.lift x).run' s = x