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

chore: prepare for unfold ident,+

Browse source
This commit is contained in:
Leonardo de Moura 2022-05-09 06:56:12 -07:00
parent e729b32b2b
commit 995d4f0979
1 changed files with 9 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/Lean/Elab/Tactic/Unfold.lean
View file

@ -20,8 +20,15 @@ def unfoldTarget (declName : Name) : TacticM Unit := do
"unfold " ident (location)?
-/
@[builtinTactic Lean.Parser.Tactic.unfold] def evalUnfold : Tactic := fun stx => do
let declName ← resolveGlobalConstNoOverload stx[1]
let loc := expandOptLocation stx[2]
withLocation loc (unfoldLocalDecl declName) (unfoldTarget declName) (throwTacticEx `unfold · m!"did not unfold '{declName}'")
if stx[1].isIdent then
go stx[1] loc
else
for declNameId in stx[1].getSepArgs do
go declNameId loc
where
go (declNameId : Syntax) (loc : Location) : TacticM Unit := do
let declName ← resolveGlobalConstNoOverload declNameId
withLocation loc (unfoldLocalDecl declName) (unfoldTarget declName) (throwTacticEx `unfold · m!"did not unfold '{declName}'")
end Lean.Elab.Tactic