fix: backtrack at `injection` failure

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.74k stars 427 forks source link

fix: backtrack at `injection` failure #6109

Closed leodemoura closed 1 week ago

leodemoura commented 1 week ago

This PR fixes an issue in the injection tactic. This tactic may execute multiple sub-tactics. If any of them fail, we must backtrack the partial assignment. This issue was causing the error: "mvarId is already assigned" in issue #6066. The issue is not yet resolved, as the equation generator for the match expressions is failing in the example provided in this issue.

leanprover-community-bot commented 1 week ago

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b8a13ab755317e4af3a4a99bd92fae26aa6a75b2 --onto a074bd9a2bd20cc470fbff4f80f2cd7b51ec0d0a. (2024-11-18 02:22:57)