Zulip Chat Archive

Stream: general

Topic: Instance docstring

Yury G. Kudryashov (Oct 22 2021 at 19:16):

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 (Oct 22 2021 at 19:21):

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

Eric Wieser (Oct 22 2021 at 19:52):

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

Patrick Massot (Oct 22 2021 at 20:40):

Widgets were already a huge progress here.

Wojciech Nawrocki (Oct 22 2021 at 22:15):

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 (Oct 23 2021 at 08:10):

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

Yury G. Kudryashov (Oct 23 2021 at 15:42):

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

Wojciech Nawrocki (Oct 23 2021 at 16:14):

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

Last updated: Dec 20 2023 at 11:08 UTC