Zulip Chat Archive

Stream: general

Topic: open_locale docstrings


Johan Commelin (Jun 03 2020 at 10:12):

Can we turn (for example) https://github.com/leanprover-community/mathlib/pull/2932/files#diff-5fc70a6c00d9ce52e2b06b9c5762d692R136
into a docstring that will show up when you hover of the "classical" in open_locale classical?

Johan Commelin (Jun 03 2020 at 10:12):

In general it would also be nice if you could hover over open_locale nat and get a pop-up window that shows which commands are executed.


Last updated: Dec 20 2023 at 11:08 UTC