Getting the type of an equality in the infoview

Stream: lean4

[Eric Wieser]

I have an equality in my goal that I'd like to know the type of. How can I get this out of the infoview? Hovering over the = gives:

image.png

[Kyle Miller]

It would be nice if the long docstring could make use of a scrollbar. The = type is cut off at the top of the infoview window here.

[Eric Wieser]

Maybe the docstring should appear above the type not below?

[Eric Wieser]

Docstrings are a nice-to-have in the infoview, the type is essential

[Kevin Buzzard]

I have whinged about this before. I suspect it happens far more to me than most people because I typically have my font on large because I can't find my reading glasses. This "box off the screen" issue never happened for me in lean 3

[Eric Wieser]

In the short-term I would consider removing the docstring for = because it's such a common object to want to know the type of

[Sebastian Ullrich]

Relevant PR, though not a complete solution for this specific issue: https://github.com/leanprover/vscode-lean4/pull/289

[Sebastian Ullrich]

It might make sense to limit docstrings to something like 3 lines by default and have a button for unfolding further

[Max Nowak 🐉]

Sub-optimal, but you can do set_option pp.explicit true.