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

fix: revert creates natural metavariable goal (#6145)

Browse source 
This PR fixes the `revert` tactic so that it creates a `syntheticOpaque`
metavariable as the new goal, instead of a `natural` metavariable

I reported it on
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.60revert.60.20gives.20natural.20metavariable.20goal/near/483388096)
This commit is contained in:
JovanGerb 2024-11-21 23:00:57 +00:00 • committed by GitHub
parent 7f2e7e56d2
commit b7248d5295
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Meta/Tactic/Revert.lean
View file

@ -43,6 +43,7 @@ def _root_.Lean.MVarId.revert (mvarId : MVarId) (fvarIds : Array FVarId) (preser
finally
mvarId.setKind .syntheticOpaque
let mvar := e.getAppFn
mvar.mvarId!.setKind .syntheticOpaque
mvar.mvarId!.setTag tag
return (toRevert.map Expr.fvarId!, mvar.mvarId!)

10
tests/lean/run/revertMetavarKind.lean Normal file
View file

@ -0,0 +1,10 @@
import Lean.Meta
open Lean Elab Tactic
example (n : Nat) : n = n := by
revert n
run_tac do
guard (← getMainDecl).kind.isSyntheticOpaque
intro n
rfl