Feature wish: show types of top-level identifiers in definitions (on mouse hover)

[anton-trunov]

I imagine this is something like adding Check @foo. for every top-level identifier and then showing that only on mouse hover or any other UI mechanism. Not sure if this is easy to add, though. This feature could be useful when reading definitions that use unfamiliar libraries. I use something like this in my Emacs setup -- the type of the thing under the cursor is displayed in the minibuffer.

[cpitclaudel]

That would be great. I expect it would be part of #27

[insightmind]

We would love to support a feature like this for Lean 4 as well and added it to our future roadmap.
As we are currently in the process of completing Lean 4 support for Alectryon, we are also open to help and implement that feature after Lean 4 support is merged.
We would aim to implement it in an extensible way that eases future support for other languages like Coq and Lean 3.