-
Notifications
You must be signed in to change notification settings - Fork 414
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
Rewrite applies the wrong equational rule #5611
Comments
I fear that's now the expected behavior. It always has been like this for recursive functions, and has become more uniform. Using |
In other places, I've seen an error message like this
But here, it's silently applying the wrong rewrite and there's no warning or hint at what to do. |
Yes, this only happens with function definitions that have a catch-all clause in the pattern match. These lead to rewrite rules that always apply, but introduce side goals. With |
Closing as (new) expected behavior |
Is this documented somewhere? What is the new expected behavior of |
It's not new behavior of |
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
On the following example, the
rw
tactic does not unfold a function definition (as it used to prior to 4.12.0).Instead, it looks as if
rw [isZeroVar2]
appliesisZeroVar2.eq_2
which results in two unprovable subgoals:This variant does the right thing::
Versions
4.12.0
Additional Information
[Additional information, configuration or data that might be necessary to reproduce the issue]
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: