Hovering on syntax-less attributes shows no docstring

[nomeata]

Attriubutes like elab_as_elim that don't have dedicated : attr syntax don’t show anything useful when hovering on them (they show the generic “declModifiers is the collection of modifiers on a declaration:” docstring):

@[elab_as_elim] theorem subst {p : (b : α) → a = b → Prop} (h₁ : a = b) (h₂ : p a rfl) : p b h₁ := by
  cases h₁
  assumption

This is unfortunate, since these attributes do have an descr passed to registerBuiltinAttribute.

It would be good if that could be surfaced here somehow, and also make Ctrl-Click work.

Versions

Lean 4.21.0-nightly-2025-05-21

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[Rob23oba]

I'll add elab_as_elim to #8173 :-) That's at least my fix for this problem, not sure if we should expose the descrs.

[nomeata]

Ah, I forgot about that one, thanks. That may be the way to go then.