Set of rewrite rules and automation for monads in general and reader_t, state_t, except_t and option_t 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.
functor, applicative, monad, simp