docstring of an attribute

Stream: lean4

[Floris van Doorn]

I want to improve the docstrings when hovering over to_additive (and related attributes). In #19297 I moved the long doc-strings to the syntax declarations of to_additive. The attribute to_additive now shows a nice long docstring, but the attribute to_additive_change_numeral shows the uninformative
"Similar to registerParametricAttribute except that attributes do not have to be assigned in the same file as the declaration."
I don't see how my changes caused this.

Is my usage of @[inherit_doc] of the changeNumeralAttr initialization function problematic?