-
Notifications
You must be signed in to change notification settings - Fork 404
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
Identifiers in auto-tactics don't respect lexical scope #4624
Comments
This seems unlikely to work, especially if you consider that you can also call |
It's definitely tricky, and I agree that there isn't an obviously right semantics. But we do need to explain to people how to use this at some point. What is the specification for the current behavior? Is it that names in the script are resolved in the global context immediately prior to the definition, or is it that they're resolved unhygienically at the use site? The former seems like something we can document our way out of, but the test here seems to indicate the latter, which strikes me as unpredictable. |
Putting the assignment |
Another issue related to this feature is that these identifiers now show up in the .ilean files at the call-sites of those functions. E.g. |
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
PR #3328 began allowing identifiers in auto-tactics, a much-desired feature. But these identifiers don't respect lexical scope/hygiene.
Steps to Reproduce
x
:Expected behavior: I would expect the test to pass, because
x
is bound by the function's parameter namedx
. Lean's tactic language usually respects lexical scope.Actual behavior: Elaboration fails with the message
unknown identifier 'x'
Versions
This is present in the 4.9 release, as well as 4.11.0-nightly-2024-07-01 on live.lean-lang.org.
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: