leanprover
feat: syntax and delaborator for delayed assignment metavariables
It's often confusing how fun x y => ?foo elaborates as fun x y => ?m.123 x y, with no way to see how ?m.123 is connected to ?foo. This PR adds syntax for delayed assignment metavariables, where the elaborated result pretty prints as fun x y => ?foo(x, y) instead. Hovering over the expression still shows the underlying ?m.123 x y term, and hovering over foo shows whatever foo might be currently assigned to, if anything. The syntax can be turned off with set_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 ?foo above we can then later refer to fun x y => ?foo(x, y) (where ?foo(x, y) is short for ?foo(x := x, y := y)), even though the x and y binders 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).
Mathlib CI status (docs):
- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the
nightly-with-mathlibbranch. Trygit rebase a3596d953d84b3493daccdc38bd2889e817efe19 --onto 5b15e1a9f3c0d1283df7f2e2f3f1b1dc59f92cf6. (2024-02-25 06:21:04) - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the
nightly-with-mathlibbranch. Trygit rebase f35c562ef8404c69aa758ddf9483a617de863870 --onto 5f70c1ca64a2c05a5866c47b9eb80a92034433ec. (2024-07-12 18:54:28)
Will we be able to limit the scope of the metavariable in this way? e.g. ?foo(x) from your example above
@ericrbg-harmonic It lets you write ?foo(x) to assign just a value for x, but to be clear y is still in its context and you can only do this if ?foo's y is still a local variable in the current scope.
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 ?m(...) should be printed instead under some pp option? Maybe it should also be default-enabled?
