diff --git a/LeanByExample/Reference/Declarative/Local.lean b/LeanByExample/Reference/Declarative/Local.lean index 4213cc4..074ee2d 100644 --- 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 index 2fc61ef..9ee921c 100644 --- 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