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

fix: simp attributes and macro scopes

Browse source
This commit is contained in:
Sebastian Ullrich 2022-04-26 09:56:59 +02:00
parent 3cf642688b
commit 814f614369
2 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/Tactic/Simp.lean
View file

@ -185,9 +185,9 @@ where
if let some e ← Term.resolveId? simpArgTerm (withInfo := true) then
return .expr e
else
resolveExt simpArgTerm.getId
resolveExt simpArgTerm.getId.eraseMacroScopes
catch _ =>
resolveExt simpArgTerm.getId
resolveExt simpArgTerm.getId.eraseMacroScopes
else if let some e ← Term.elabCDotFunctionAlias? simpArgTerm then
return .expr e
else

5
tests/pkg/user_attr/UserAttr/Tst.lean
View file

@ -16,3 +16,8 @@ example : f x + g x = 2*x + 3 := by
example : f x = id (x + 2) := by
simp
simp [my_simp]
macro "my_simp" : tactic => `(simp [my_simp])
example : f x = id (x + 2) := by
my_simp