-
Notifications
You must be signed in to change notification settings - Fork 415
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.
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
fix: hovers on binders with metavariables #4192
Conversation
The changes to the test output looks reasonable, in one case we see that the info tree no longer contains entries from a back-tracked attempt at elaboration. |
Mathlib CI status (docs):
|
Interesting, this makes the unused-variable-linter better (see leanprover-community/batteries#802) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This looks good to me (auto implicits should act as if they were always there, right?), though it'd be good to get another opinion since I'm not completely sure why restore
doesn't restore info trees to begin with.
I don't know. It might be good to double-check and document the need for this parameter but that shouldn't hold back this PR. |
IIRC the original intent was to retain information from overloading but it seems some (all?) of that was switched to |
this fixes #4078. It is an alternative fix to the one in #4137, suggested
by @kmill.
Incidentially, it makes the unused variable linter better. My theory is that
if we don’t reset the info when backtracking, the binder shows up more than
once in the info tree, and then it is considered “used”, although there are
just multiple binders.