Created
May 6, 2025 20:54
-
-
Save PhotonQuantum/55f74e1a3dcce8740bd5f5c7c5403b99 to your computer and use it in GitHub Desktop.
Lean4: clear inaccessible hypotheses
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| open Lean Meta Elab Tactic in | |
| def clearInaccessibles (mvarId : MVarId) : TacticM MVarId := do | |
| let mvarDecl ← mvarId.getDecl | |
| let mut lctx := mvarDecl.lctx | |
| let mut info := #[] | |
| let mut found : NameSet := {} | |
| let n := lctx.numIndices | |
| for i in [:n] do | |
| let j := n - i - 1 | |
| match lctx.getAt? j with | |
| | none => pure () | |
| | some localDecl => | |
| if localDecl.isImplementationDetail then | |
| continue | |
| let shadowed := found.contains localDecl.userName | |
| if shadowed then | |
| lctx := lctx.erase localDecl.fvarId | |
| found := found.insert localDecl.userName | |
| let mvarNew ← mkFreshExprMVarAt lctx mvarDecl.localInstances mvarDecl.type MetavarKind.syntheticOpaque mvarDecl.userName | |
| withSaveInfoContext <| mvarNew.mvarId!.withContext do | |
| for (fvarId, stx) in info do | |
| Term.addLocalVarInfo stx (mkFVar fvarId) | |
| mvarId.assign mvarNew | |
| return mvarNew.mvarId! | |
| open Lean Elab Tactic in | |
| elab "clear_i": tactic => do | |
| replaceMainGoal [← clearInaccessibles (← getMainGoal)] |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment