feat: add option pp.mvars.delayed
#5643
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Where before we had ```lean #check fun x : Nat => ?a -- fun x ↦ ?m.7 x : (x : Nat) → ?m.6 x ``` Now by default we have ```lean #check fun x : Nat => ?a -- fun x => ?a : (x : Nat) → ?m.6 x ``` in particular, delayed assignment metavariables such as `?m.7` pretty print using the name of the metavariable they are delayed assigned to, suppressing the arguments used in the delayed assignment (hence `?a` rather than `?a x`). Hovering over `?a` shows `?m.7 x`. The benefit is that users can see the user-provided name in local contexts. The original pretty printing behavior can be recovered using `set_option pp.mvars.delayed true`. This PR also extends the documentation for holes and synthetic holes, with useful high-level technical details about what delayed assignments are. (This PR supercedes leanprover#3494, which has a round-trippable notation for delayed assignments. The notation in this PR is unlikely to round trip, but it is better than the current situation, where delayed assignment metavariables never round trip.)
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Oct 7, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 7, 2024
|
Mathlib CI status (docs):
|
leanprover-community-bot
added
the
builds-mathlib
nomeata
approved these changes
Oct 8, 2024
src/Lean/Parser/Term.lean
Outdated
Comment on lines
176
to
178
| ## Delayed assigned metavariables | ||
|
|
||
| This section gives a high-level overview of technical details of synthetic holes, which you should feel free to skip. |
There was a problem hiding this comment.
Good to write this up! But I’m wary of putting it anywhere where a beginner could accidentially stumble over it, such as hovers. In general, this is probably too long for a hover docstring. It should probably go into the reference manual and the docstring could indicate that there is more deeply technical information there.
Not sure if this should hold up the present PR, though; we could merge as it is right now and doc-refactor later.
There was a problem hiding this comment.
I agree. I've just added some more warnings not to read the section :-)
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Oct 8, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 8, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Oct 8, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 8, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Where before we had
Now by default we have
In particular, delayed assignment metavariables such as
?m.7pretty print using the name of the metavariable they are delayed assigned to, suppressing the bound variables used in the delayed assignment (hence?arather than?a x). Hovering over?ashows?m.7 x.The benefit is that users can see the user-provided name in local contexts. A justification for this pretty printing choice is that
?m.7 xis supposed to stand for?a, and furthermore it is just as opaque to assignment in defeq as?ais (however, when synthetic opaque metavariables are made assignable, delayed assignments can be a little less assignable than true synthetic opaque metavariables).The original pretty printing behavior can be recovered using
set_option pp.mvars.delayed true.This PR also extends the documentation for holes and synthetic holes, with some technical details about what delayed assignments are. This likely should be moved to the reference manual, but for now it is included in this docstring.
(This PR is a simplified version of #3494, which has a round-trippable notation for delayed assignments. The pretty printing in this PR is unlikely to round trip, but it is better than the current situation, which is that delayed assignment metavariables never round trip, and plus it does not require introducing a new notation.)