local と scoped の構文的な共通点を強調する

lean-ja · Nov 16, 2024 · f4d7c1f · f4d7c1f
1 parent 407bbf3
commit f4d7c1f
Show file tree

Hide file tree

Showing 2 changed files with 27 additions and 3 deletions.
diff --git a/LeanByExample/Reference/Declarative/Local.lean b/LeanByExample/Reference/Declarative/Local.lean
@@ -41,7 +41,8 @@ namespace hoge
   #check_failure succ'
 end hoge
 
-/- `local` で有効範囲を限定できるコマンドには、次のようなものがあります。
+/- ## 修飾可能なコマンド
+`local` で有効範囲を限定できるコマンドには、次のようなものがあります。
 * [`elab`](./Elab.md), `elab_rules`
 * [`infix`](./Infix.md), `infil`, `infixr`
 * [`macro`](./Macro.md), [`macro_rules`](./MacroRules.md)
@@ -55,7 +56,7 @@ end hoge
 リストの全体は、`local` の後に修飾できないコマンドを続けたときのエラーメッセージで確認できます。
 -/
 
-open Lean Parser
+open Lean Parser in
 
 /-- parse できるかどうかチェックする関数 -/
 def checkParse (cat : Name) (s : String) : MetaM Unit := do
@@ -117,3 +118,14 @@ end
 -- section を抜けると simp 補題が利用できなくなる
 #guard_msgs (drop warning) in --#
 #check_failure (by simp : MyNat.add .zero .zero = .zero)
+
+/- ## 構文的な性質
+[`local`](./Local.md) と [`scoped`](./Scoped.md) はともに構文的には `attrKind` に相当します。
+-/
+
+/-- 例示のための意味のないコマンド -/
+macro attrKind "#greet " : command => `(#eval "hello")
+
+-- パース出来るので、`local` と `scoped` は同じカテゴリに属する
+local #greet
+scoped #greet
diff --git a/LeanByExample/Reference/Declarative/Scoped.lean b/LeanByExample/Reference/Declarative/Scoped.lean
@@ -33,7 +33,8 @@ section
   #greet
 end
 
-/- `scoped` で有効範囲を限定できるコマンドには、次のようなものがあります。
+/- ## 修飾可能なコマンド
+`scoped` で有効範囲を限定できるコマンドには、次のようなものがあります。
 * [`elab`](./Elab.md), `elab_rules`
 * [`infix`](./Infix.md), `infixl`, `infixr`
 * [`instance`](./Instance.md)
@@ -100,3 +101,14 @@ section
   #guard_msgs (drop warning) in --#
   #check_failure greet
 end
+
+/- ## 構文的な性質
+[`local`](./Local.md) と [`scoped`](./Scoped.md) はともに構文的には `attrKind` に相当します。
+-/
+
+/-- 例示のための意味のないコマンド -/
+macro attrKind "#greet " : command => `(#eval "hello")
+
+-- パース出来るので、`local` と `scoped` は同じカテゴリに属する
+local #greet
+scoped #greet