lean4-mode
lean4-mode copied to clipboard
Hover docs in info view
These are available in the fork https://github.com/ultronozm/lean4-mode and I would be happy to upstream them here once eglot is available here as an lsp backend.
There is the further issue of how best to achieve "recursive hovering". I've managed this crudely using the mini-package https://github.com/ultronozm/eldoc-icebox.el, together with a hook that sets up the Lean4 hover docs. I figure this can be discussed once the basic support is upstreamed.