You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
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.The text was updated successfully, but these errors were encountered: