Redefining the elaborator for the `simp` attribute

Stream: lean4

[Simon Hudon]

I just wrote this code but attr isn't recognized.

elab_rules : attr
| `(simp $x $y $z) => _
-- unsupported syntax category 'attr'

Since it was declared as

syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (prio)? : attr

in Init/Notation.lean. I take it changing the behavior of @[simp] is not done by writing an elab_rules. Is it still possible? If so, how?