From 814f61436901597a60ea47385ca164cf5d2ef687 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 26 Apr 2022 09:56:59 +0200 Subject: [PATCH] fix: simp attributes and macro scopes --- src/Lean/Elab/Tactic/Simp.lean | 4 ++-- tests/pkg/user_attr/UserAttr/Tst.lean | 5 +++++ 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index 589481e4fd..29ddb0c930 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -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 diff --git a/tests/pkg/user_attr/UserAttr/Tst.lean b/tests/pkg/user_attr/UserAttr/Tst.lean index 350d9e2099..d40fe1391e 100644 --- a/tests/pkg/user_attr/UserAttr/Tst.lean +++ b/tests/pkg/user_attr/UserAttr/Tst.lean @@ -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