Useless hover on docstrings

Stream: new members

[Dan Abramov]

Not sure if worth reporting as a bug so I'll ask here first.

This hover is often making me sad:

Screenshot 2025-08-23 at 13.13.48.png

What I actually am trying to hover on is stuff like @[pp_using_anonymous_constructor] or something specific in the docstring. But I always get a docstring telling me that you can add docstrings. That's cool I guess! But it's useless after the first time you see it.

In general, it feels weird that some bit of internal naming (declModifiers in this case) shows up in this case. I can understand why this happens (Lean is super extensible, and docstring support itself is probably tacked onto it somewhere, and I'm looking at the docs for the part that defines this syntax, which happens to be called declModifiers). But if I wear my "Lean user" hat, this feels like something internal peeking through.

[Dan Abramov]

The main problem though is that I can't click into pp_using_anonymous_constructor and so I can't read where it's defined or what it does.

[Robin Arnez]

You are probably on an older version:
Screenshot 2025-08-23 160417.png

[Robin Arnez]

specifically, lean4#8173 added this which should be part of Lean v4.22.0

[Robin Arnez]

And clicking on the attribute should lead you to docs#Lean.ppUsingAnonymousConstructorAttr