# 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

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

## Equations

- StateT.equiv F = F

## Instances For

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

## Equations

- ReaderT.equiv F = F