# Monad #

## Attributes #

- ext
- functor_norm
- monad_norm

## Implementation Details #

Set of rewrite rules and automation for monads in general and
`ReaderT`

, `StateT`

, `ExceptT`

and `OptionT`

in particular.

The rewrite rules for monads are carefully chosen so that `simp with functor_norm`

will not introduce monadic vocabulary in a context where
applicatives would do just fine but will handle monadic notation
already present in an expression.

In a context where monadic reasoning is desired `simp with monad_norm`

will translate functor and applicative notation into monad notation
and use regular `functor_norm`

rules as well.

## Tags #

functor, applicative, monad, simp

def
StateT.eval
{σ : Type u}
{α : Type u}
{m : Type u → Type v}
[inst : Functor m]
(cmd : StateT σ m α)
(s : σ)
:

m α

run a `StateT`

program and discard the final state

## Equations

- StateT.eval cmd s = Prod.fst <$> StateT.run cmd s

def
StateT.equiv
{σ₁ : Type u₀}
{α₁ : Type u₀}
{σ₂ : Type u₁}
{α₂ : Type u₁}
{m₁ : Type u₀ → Type v₀}
{m₂ : Type u₁ → Type v₁}
(F : (σ₁ → m₁ (α₁ × σ₁)) ≃ (σ₂ → m₂ (α₂ × σ₂)))
:

reduce the equivalence between two state monads to the equivalence between their respective function spaces

## Equations

- StateT.equiv F = F