search

cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
227 stars 36 forks source link

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

Open anton-trunov opened 2 years ago

anton-trunov commented 2 years ago

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 commented 2 years ago

That would be great. I expect it would be part of https://github.com/cpitclaudel/alectryon/issues/27

insightmind commented 2 years ago

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.