コードを簡略化する

Co-authored-by: spinylobster <[email protected]>
lean-ja · Nov 16, 2024 · e08be94 · e08be94
1 parent 0caf409
commit e08be94
Showing 1 changed file with 1 addition and 4 deletions.
diff --git a/LeanByExample/Reference/Declarative/DeclareAesopRuleSets.lean b/LeanByExample/Reference/Declarative/DeclareAesopRuleSets.lean
@@ -45,10 +45,7 @@ example : True := by
 
 /-- `hoge` タクティク用のルールを追加する -/
 macro attrKind:attrKind "add_hoge_rules" e:Aesop.rule_expr : command =>
-  match attrKind with
-  | `(attrKind| local) => `(command| local add_aesop_rules (rule_sets := [HogeRules]) $e)
-  | `(attrKind| scoped) => `(command| scoped add_aesop_rules (rule_sets := [HogeRules]) $e)
-  | _ => `(command| add_aesop_rules (rule_sets := [HogeRules]) $e)
+  `(command| $attrKind:attrKind add_aesop_rules (rule_sets := [HogeRules]) $e)
 
 namespace Command --#