In mathlib3 [we wrote](https://github.com/leanprover-community/mathlib/blob/master/src/control/monad/basic.lean#L38): ``` mk_simp_attribute monad_norm none with functor_norm ``` but `register_simp_attr` does not support a `with` clause.