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