max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: unfold should fail if it didn't unfold anything

Browse source
This commit is contained in:
Leonardo de Moura 2022-05-09 06:41:17 -07:00
parent 4875224bd4
commit e729b32b2b
3 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/Tactic/Unfold.lean
View file

@ -33,11 +33,13 @@ where
def unfoldTarget (mvarId : MVarId) (declName : Name) : MetaM MVarId := withMVarContext mvarId do
let target ← instantiateMVars (← getMVarType mvarId)
let r ← unfold target declName
if r.expr == target then throwError "tactic 'unfold' failed to unfold '{declName}' at{indentExpr target}"
applySimpResultToTarget mvarId target r
def unfoldLocalDecl (mvarId : MVarId) (fvarId : FVarId) (declName : Name) : MetaM MVarId := withMVarContext mvarId do
let localDecl ← getLocalDecl fvarId
let r ← unfold (← instantiateMVars localDecl.type) declName
if r.expr == localDecl.type then throwError "tactic 'unfold' failed to unfold '{declName}' at{indentExpr localDecl.type}"
let some (_, mvarId) ← applySimpResultToLocalDecl mvarId fvarId r (mayCloseGoal := false) | unreachable!
return mvarId

5
tests/lean/unfoldFailure.lean Normal file
View file

@ -0,0 +1,5 @@
example : True := by
unfold Nat.add
example (h : x = 2 * y) : True := by
unfold Nat.add at h

4
tests/lean/unfoldFailure.lean.expected.out Normal file
View file

@ -0,0 +1,4 @@
unfoldFailure.lean:2:2-2:16: error: tactic 'unfold' failed to unfold 'Nat.add' at
True
unfoldFailure.lean:5:2-5:21: error: tactic 'unfold' failed to unfold 'Nat.add' at
x = 2 * y