Instance docstring

Stream: general

[Yury G. Kudryashov]

Is there a reasonable way to make lean server tell the editor the name of the instance responsible for has_mul in this particular a * b? I understand that this is not a trivial problem but sometimes I see a * b on a non-trivial type and wonder where the corresponding has_mul is defined.

[Gabriel Ebner]

I'd keep this in mind as a todo for Lean 4.

[Eric Wieser]

You can eventually get it through the widget view, right?

[Patrick Massot]

Widgets were already a huge progress here.

[Wojciech Nawrocki]

You can eventually get it through the widget view, right?

Yep, you should be able to hover over a * b in the view, then click on the type.has_mul instance, no? In Lean 4 you will (once we resolve some bugs..) also be able to do this in the infoview on #check a*b assuming these are closed terms.

[Kevin Buzzard]

I think Yury might use Emacs? On VS code this is indeed easy

[Yury G. Kudryashov]

It seems that now I have more and more reasons to either implement widgets client in Emacs, or switch to neovim.

[Wojciech Nawrocki]

I see. I made an issue for Emacs widgets in Lean 4 here.