Lemmas about StateT

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

Equations

• StateT.instMonadLift_toMathlib = { monadLift := fun {α : Type ?u.38} (x : StateT σ m α) => StateT.mk fun (s : σ) => liftM (x.run s) }

@[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 = StateT.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

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 : α) : (StateT.mk fun (s : σ) => pure (x, s)) = pure x