Skip to content
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.

Sign up for GitHub

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

fix: make rewrite/rw tactic abort on elaboration errors #6891

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
+26 −0
Open

fix: make rewrite/rw tactic abort on elaboration errors #6891

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions src/Lean/Elab/Tactic/Rewrite.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,8 @@ open Meta
def rewriteTarget (stx : Syntax) (symm : Bool) (config : Rewrite.Config := {}) : TacticM Unit := do
Term.withSynthesize <| withMainContext do
let e ← elabTerm stx none true
if e.hasSyntheticSorry then
throwAbortTactic
let r ← (← getMainGoal).rewrite (← getMainTarget) e symm (config := config)
let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof
replaceMainGoal (mvarId' :: r.mvarIds)
Expand All @@ -25,6 +27,8 @@ def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Re
-- See issues #2711 and #2727.
let rwResult ← Term.withSynthesize <| withMainContext do
let e ← elabTerm stx none true
if e.hasSyntheticSorry then
throwAbortTactic
let localDecl ← fvarId.getDecl
(← getMainGoal).rewrite localDecl.type e symm (config := config)
let replaceResult ← (← getMainGoal).replaceLocalDecl fvarId rwResult.eNew rwResult.eqProof
Expand Down
22 changes: 22 additions & 0 deletions tests/lean/run/rwWithElabError.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
/-!
# Test for error reporting when `rw`/`rewrite` has an elaboration error
-/

/-!
Elaboration failures abort tactic evaluation.
Before, the second error was
```
error: tactic 'rewrite' failed, equality or iff proof expected
?m.5
⊢ True
```
-/
/--
error: unknown identifier 'not_a_theorem'
---
error: unsolved goals
⊢ True
-/
#guard_msgs in
example : True := by
rewrite [not_a_theorem]
Loading