Skip to content

Hover docs in info view #94

@ultronozm

Description

@ultronozm

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions