Fixing attribute go to definition

Stream: mathlib4

[Julian Berman]

I am trying to make register_simp_attr annotate the new attribute with where to jump to for go to definition. For example, to make go to definition on simp [parity_simps] jump to the register_simp_attr parity_simps line, which at very least is better than where it currently jumps to (which is to the definition of simp in core). Even better would be if the docstring -- which seems to be used to annotate the register_simp_attr lines in Mathlib -- would show up for the registered attribute on hover, and even better better IMO would be to automatically append it to the definition of the relevant other declarations (e.g. in this case appending it to Even that when using it you probably are interested in the parity_simps attribute). Can someone give me some breadcrumbs on which things are used to affect this behavior?

[Joachim Breitner]

for the docstring at least https://github.com/leanprover/lean4/pull/5838 may be relevant or related