Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix: consistently show non-mvar term in hovertext #5368

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

fix: consistently show non-mvar term in hovertext #5368

wants to merge 1 commit into from

Commits on Sep 16, 2024

  1. fix: consistently show non-mvar term in hovertext 

    Previously, the hover text would only show the term
in the hovertext if the pretty-printed text was 'atomic',
which excluded expressions like `1 + 1`.
This made the hovertext less useful for inspecting an underscore (`_`),
since only the type (and not the term) would be displayed
for a complex expression.

Change the behavior to hide the term if it's a single
metavariable, and otherwise display both the term and type.
This ensures that we do not produce unhelpful hovertext
like `?m : SomeType` (we still produce just `SomeType`).

We now display both the term and type in a few other cases -
this makes the output a little more verbose, but also ensures
that users can see resolved metavariables in the term.

Closes leanprover#5367
    @Aaron1011
    Aaron1011 committed Sep 16, 2024
    Configuration menu
    Copy the full SHA
    ace0538 View commit details
    Browse the repository at this point in the history