From 5eebbba369da5f0cf2d3df52f6dc9aa7dcb19478 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 16 Nov 2024 14:52:38 +0900 Subject: [PATCH] =?UTF-8?q?`add=5Fhoge=5Frules`=20=E3=82=B3=E3=83=9E?= =?UTF-8?q?=E3=83=B3=E3=83=89=E3=81=AB=20`local`=20=E3=82=84=20`scoped`=20?= =?UTF-8?q?=E3=82=92=E4=BB=98=E4=B8=8E=E3=81=A7=E3=81=8D=E3=81=AA=E3=81=84?= =?UTF-8?q?=20Fixes=20#1118?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../Reference/Declarative/DeclareAesopRuleSets.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/LeanByExample/Reference/Declarative/DeclareAesopRuleSets.lean b/LeanByExample/Reference/Declarative/DeclareAesopRuleSets.lean index 6c2617c..3612a52 100644 --- a/LeanByExample/Reference/Declarative/DeclareAesopRuleSets.lean +++ b/LeanByExample/Reference/Declarative/DeclareAesopRuleSets.lean @@ -44,8 +44,11 @@ example : True := by /- `hoge` タクティク用のルールを登録するのは [`add_aesop_rules`](./AddAesopRules.md) コマンドで可能ですが、これに対しても専用のコマンドを用意することができます。-/ /-- `hoge` タクティク用のルールを追加する -/ -macro "add_hoge_rules" e:Aesop.rule_expr : command => - `(command| add_aesop_rules (rule_sets := [HogeRules]) $e) +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) namespace Command --# @@ -60,7 +63,7 @@ example : MyTrue := by apply MyTrue.intro -- `MyTrue` に関するルールを `hoge` に登録する -add_hoge_rules safe constructors [MyTrue] +local add_hoge_rules safe constructors [MyTrue] example : MyTrue := by -- `hoge` で証明できるようになった! @@ -82,7 +85,7 @@ macro "hoge" e:Aesop.rule_expr : attr => namespace Attr --# /-- `True` を模して自作した命題 -/ -@[hoge safe constructors] +@[local hoge safe constructors] inductive MyTrue : Prop where | intro