feat: syntax and delaborator for delayed assignment metavariables #3494
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
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
|
Will we be able to limit the scope of the metavariable in this way? e.g. |
|
@ericrbg-harmonic It lets you write |
|
I am concerned about the size of this expression, as I often see these metavariables in printouts and I generally don't actually care about the values of the arguments and only the fact that it is a metavariable (possibly an unassignable metavariable) is relevant to me. Maybe |
kmill
force-pushed
the
pp_delayed_assignment
branch
from
195ce1c to
7b90837
Compare
kmill
force-pushed
the
pp_delayed_assignment
branch
from
7b90837 to
c4ee28d
Compare
leodemoura
force-pushed
the
master
branch
2 times, most recently
from
32d60c5 to
696f70b
Compare
kmill
added a commit
to kmill/lean4
that referenced
this pull request
Oct 7, 2024
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-merge-queue bot
pushed a commit
that referenced
this pull request
Oct 8, 2024
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 bound variables 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. A justification for this pretty printing choice is that `?m.7 x` is supposed to stand for `?a`, and furthermore it is just as opaque to assignment in defeq as `?a` is (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.)
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.
It's often confusing how
fun x y => ?fooelaborates asfun x y => ?m.123 x y, with no way to see how?m.123is connected to?foo. This PR adds syntax for delayed assignment metavariables, where the elaborated result pretty prints asfun x y => ?foo(x, y)instead. Hovering over the expression still shows the underlying?m.123 x yterm, and hovering overfooshows whateverfoomight be currently assigned to, if anything. The syntax can be turned off withset_option pp.mvars.delayed false.This also adds an elaborator for
?foo(x := a, y := b)syntax to create a new delayed assignment metavariable from a metavariable, making the pretty printed syntax elaboratable. In addition to being for making pretty printing round trip, it is filling in a missing feature, since, as a user, it's impossible to use synthetic holes in incompatible local contexts without being able to specify delayed assignments. For example, with the?fooabove we can then later refer tofun x y => ?foo(x, y)(where?foo(x, y)is short for?foo(x := x, y := y)), even though thexandybinders are totally new fvars.The syntax is chosen to (1) use parentheses with no whitespace since that is reserved for new syntax, (2) to resemble structure instance notation, and (3) to be something like the Lean version of lambda calculus substitution (and in any case, square brackets are already used by GetElem).