Functor Laws, applicative laws, and monad Laws

theorem StateT.map_const {σ : Type u} {m : Type u → Type v} {α β : Type u} [Monad m] : Functor.mapConst = Functor.map ∘ Function.const β

A copy of LawfulFunctor.map_const for StateT that holds even if m is not lawful.

@[simp]

theorem StateT.run_mapConst {σ : Type u} {m : Type u → Type v} {α β : Type u} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : β) (st : σ) : (Functor.mapConst y x).run st = Prod.map (Function.const α y) id <$> x.run st

@[simp]

theorem ExceptT.run_monadLift {α ε : Type u} {m : Type u → Type v} {n : Type u → Type u_1} [Monad m] [MonadLiftT n m] (x : n α) : (monadLift x).run = Except.ok <$> monadLift x