Monad
Attributes
- ext
- functor_norm
- monad_norm
Implementation Details
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.
Tags
functor, applicative, monad, simp
reduce the equivalence between two state monads to the equivalence between their respective function spaces
reduce the equivalence between two reader monads to the equivalence between their respective function spaces