修飾子を宣言的コマンドから独立させる

LeanByExample/Declarative/Attribute.lean

@@ -75,7 +75,7 @@ example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
   simp
 
 /- ## 有効範囲を制限する
-特定の [`section`](./Section.md) でのみ付与した属性を有効にするには、[`local`](./Local.md) で属性名を修飾します。
+特定の [`section`](./Section.md) でのみ付与した属性を有効にするには、[`local`](#{root}/Modifier/Local.md) で属性名を修飾します。
 -/
 example (P Q : Prop) : ((P ∨ Q) ∧ ¬ Q) ↔ (P ∧ ¬ Q) := by
   -- simp だけでは証明が終わらない

LeanByExample/Declarative/Axiom.lean

@@ -203,7 +203,7 @@ theorem my_funext {f g : (x : α) → β x} (h : ∀ x, f x = g x) : f = g := by
 #guard_msgs in #print axioms my_funext
 
 /- ### 選択原理 Classical.choice { #ClassicalChoice }
-選択原理は、ある型が空ではないという情報だけから、「魔法のように」具体的な元を構成することができると主張します。これは計算不可能な操作であるため、選択原理を使用する関数には [`noncomputable`](./Noncomputable.md) 修飾子が必要になります。
+選択原理は、ある型が空ではないという情報だけから、「魔法のように」具体的な元を構成することができると主張します。これは計算不可能な操作であるため、選択原理を使用する関数には [`noncomputable`](#{root}/Modifier/Noncomputable.md) 修飾子が必要になります。
 
 選択原理は数学でいうと NBG(Neumann-Bernays-Gödel) 集合論における大域選択公理(axiom of global choice)とよく似ています。
 -/

LeanByExample/Declarative/Opaque.lean

@@ -3,7 +3,7 @@
 
 ## def との違い
 
-[`def`](./Def.md) と異なり `opaque` コマンドを使用して宣言した名前は、`#reduce` コマンドで簡約できません。
+[`def`](./Def.md) コマンドと異なり `opaque` コマンドを使用して宣言した名前は、`#reduce` コマンドで簡約できません。
 -/
 
 -- def を使って定義
@@ -29,7 +29,7 @@ opaque opaque_greet : String := "hello world!"
 /-- info: opaque_greet -/
 #guard_msgs in #reduce opaque_greet
 
-/- `opaque` で宣言された名前は [`partial`](./Partial.md) で修飾された名前と同様に証明の中で簡約できなくなり、コンパイラを信頼しないとそれに関する証明ができなくなります。-/
+/- `opaque` で宣言された名前は [`partial`](#{root}/Modifier/Partial.md) で修飾された名前と同様に証明の中で簡約できなくなり、コンパイラを信頼しないとそれに関する証明ができなくなります。-/
 
 -- 等しいものだという判定はできる
 #eval opaque_greet == greet

LeanByExample/Declarative/Section.lean

@@ -5,7 +5,7 @@
 * [`variable`](./Variable.md) で定義された引数の有効範囲を制限する。
 * [`open`](./Open.md) で開いた名前空間の有効範囲を制限する。
 * [`set_option`](./SetOption.md) で設定したオプションの有効範囲を制限する。
-* [`local`](./Local.md) で修飾されたコマンドの有効範囲を制限する。
+* [`local`](#{root}/Modifier/Local.md) で修飾されたコマンドの有効範囲を制限する。
 
 `section` コマンドで開いたセクションは `end` で閉じることができますが、`end` は省略することもできます。`end` を省略した場合はそのファイルの終わりまでが有効範囲となります。
 

LeanByExample/Declarative/Local.lean → LeanByExample/Modifier/Local.lean

@@ -1,5 +1,5 @@
 /- # local
-`local` はコマンドをその [`section`](./Section.md) の内部でだけ有効にするための修飾子です。
+`local` はコマンドをその [`section`](#{root}/Declarative/Section.md) の内部でだけ有効にするための修飾子です。
 -/
 import Lean --#
 section foo
@@ -20,7 +20,7 @@ section foo
   #check_failure succ'
 end foo
 
-/- コマンドの有効範囲を [`namespace`](./Namespace.md) の内部に限定するのにも使えます。ただし、下記のコードで示しているように、`local` で修飾したコマンドの効果は同じ名前空間の中で永続するのではなく、`end` でその名前空間が閉じられたときに消失します。-/
+/- コマンドの有効範囲を [`namespace`](#{root}/Declarative/Namespace.md) の内部に限定するのにも使えます。ただし、下記のコードで示しているように、`local` で修飾したコマンドの効果は同じ名前空間の中で永続するのではなく、`end` でその名前空間が閉じられたときに消失します。-/
 
 namespace hoge
   -- local を付けて新しい記法を定義
@@ -43,14 +43,14 @@ end hoge
 
 /- ## 修飾可能なコマンド
 `local` で有効範囲を限定できるコマンドには、次のようなものがあります。
-* [`elab`](./Elab.md), `elab_rules`
-* [`infix`](./Infix.md), `infil`, `infixr`
-* [`macro`](./Macro.md), [`macro_rules`](./MacroRules.md)
-* [`notation`](./Notation.md)
-* [`postfix`](./Postfix.md)
-* [`prefix`](./Prefix.md)
-* [`instance`](./Instance.md)
-* [`syntax`](./Syntax.md)
+* [`elab`](#{root}/Declarative/Elab.md), `elab_rules`
+* [`infix`](#{root}/Declarative/Infix.md), `infil`, `infixr`
+* [`macro`](#{root}/Declarative/Macro.md), [`macro_rules`](#{root}/Declarative/MacroRules.md)
+* [`notation`](#{root}/Declarative/Notation.md)
+* [`postfix`](#{root}/Declarative/Postfix.md)
+* [`prefix`](#{root}/Declarative/Prefix.md)
+* [`instance`](#{root}/Declarative/Instance.md)
+* [`syntax`](#{root}/Declarative/Syntax.md)
 * などなど
 
 リストの全体は、`local` の後に修飾できないコマンドを続けたときのエラーメッセージで確認できます。
@@ -93,7 +93,7 @@ end
 #check_failure (0 : MyNat)
 
 /- ## 属性に対する local
-属性付与の効果範囲を限定するためには、[`attribute`](./Attribute.md) コマンドを `local` で修飾するのではなく、`attribute` コマンドの中で `local` を使います。
+属性付与の効果範囲を限定するためには、[`attribute`](#{root}/Declarative/Attribute.md) コマンドを `local` で修飾するのではなく、`attribute` コマンドの中で `local` を使います。
 -/
 
 def MyNat.add (n m : MyNat) : MyNat :=

LeanByExample/Declarative/Noncomputable.lean → LeanByExample/Modifier/Noncomputable.lean

@@ -1,9 +1,9 @@
 /- # noncomputable
 `noncomputable` は、宣言された関数が計算可能でないことを Lean に伝えるために使われます。
 
-Lean は、[`def`](./Def.md) で定義された関数はすべて計算可能であると想定しています。したがって、計算可能でない関数を定義すると、エラーが発生します。
+Lean は、[`def`](#{root}/Declarative/Def.md) コマンドで定義された関数はすべて計算可能であると想定しています。したがって、計算可能でない関数を定義すると、エラーが発生します。
 
-計算可能でない関数が生じるのは、選択原理 [`Classical.choice`](./Axiom.md#ClassicalChoice) を使用したときです。選択原理は、型が「空ではない」という証明だけから、その型の項を魔法のように構成できると主張している公理です。`Prop` の[証明無関係](../Type/Prop.md#ProofIrrel)という特性により、空ではないという情報から具体的な項の情報は得られないため、選択原理を使用した関数は計算不能になります。
+計算可能でない関数が生じるのは、選択原理 [`Classical.choice`](#{root}/Declarative/Axiom.md#ClassicalChoice) を使用したときです。選択原理は、型が「空ではない」という証明だけから、その型の項を魔法のように構成できると主張している公理です。`Prop` の[証明無関係](../Type/Prop.md#ProofIrrel)という特性により、空ではないという情報から具体的な項の情報は得られないため、選択原理を使用した関数は計算不能になります。
 -/
 
 variable {X Y : Type}
@@ -42,7 +42,7 @@ noncomputable def inverse (f : X → Y) (hf : Surjective f) : Y → X := by
   have x := Classical.choice this
   exact x.val
 
-/- `noncomputable` とマークされた式を含む式は文字通り評価不能になり、[`#eval`](../Diagnostic/Eval.md) に渡すことができなくなります。-/
+/- `noncomputable` とマークされた式を含む式は文字通り評価不能になり、[`#eval`](#{root}/Diagnostic/Eval.md) に渡すことができなくなります。-/
 
 -- 補助として `id` という恒等写像が全射であることを示しておく
 theorem id_surjective : Surjective (id : Nat → Nat) := by

LeanByExample/Declarative/Partial.lean → LeanByExample/Modifier/Partial.lean

@@ -59,7 +59,7 @@ partial def forever (x : Int) : Int :=
 -- more 関数も停止しないが、partial は不要である
 def more := @forever
 
-/- これは意外に思えます。`partial` とマークされた関数は停止性が保証されていないので、それを使用した関数も停止性を保証できなくなるはずだからです。なぜこうなるのかというと、`partial` はそもそも「停止性が保証されていない」ことを表すものではなく、[`opaque`](./Opaque.md) と同様に「名前が定義に展開できない」ことを表すものだからです。-/
+/- これは意外に思えます。`partial` とマークされた関数は停止性が保証されていないので、それを使用した関数も停止性を保証できなくなるはずだからです。なぜこうなるのかというと、`partial` はそもそも「停止性が保証されていない」ことを表すものではなく、[`opaque`](#{root}/Declarative/Opaque.md) と同様に「名前が定義に展開できない」ことを表すものだからです。-/
 
 -- 実際に #reduce を実行してみると、
 -- forever の部分が簡約されていないことがわかる

LeanByExample/Declarative/Private.lean → LeanByExample/Modifier/Private.lean

@@ -3,7 +3,7 @@
 
 不安定なAPIなど、外部に公開したくないものに対して使うのが主な用途です。
 -/
-import LeanByExample.Declarative.Protected -- protected のページをインポート
+import LeanByExample.Modifier.Protected -- protected のページをインポート
 import Lean
 namespace Private --#
 

LeanByExample/Declarative/Protected.lean → LeanByExample/Modifier/Protected.lean

@@ -67,7 +67,7 @@ end Foo
 
 /- ## protected def 以外の用法
 
-`def` コマンドに対してだけでなく、[`indudctive`](./Inductive.md) コマンドで生成されるコンストラクタに対しても使用可能です。-/
+`def` コマンドに対してだけでなく、[`indudctive`](#{root}/Declarative/Inductive.md) コマンドで生成されるコンストラクタに対しても使用可能です。-/
 section --#
 
 /-- 2分木 -/
@@ -88,7 +88,7 @@ open BinTree
 #check empty
 
 end --#
-/- また [`structure`](./Structure.md) コマンドで生成されるアクセサ関数やコンストラクタに対しても使用可能です。  -/
+/- また [`structure`](#{root}/Declarative/Structure.md) コマンドで生成されるアクセサ関数やコンストラクタに対しても使用可能です。 -/
 section --#
 structure Sample where
   -- コンストラクタも protected にできる

LeanByExample/Modifier/README.lean

@@ -0,0 +1,4 @@
+/- # 修飾子
+
+本書では、必ず後ろにトップレベルコマンドが続いて、後続のコマンドに影響を与える構文要素のことを便宜的に修飾子と呼んでいます。
+-/

LeanByExample/Declarative/Scoped.lean → LeanByExample/Modifier/Scoped.lean

@@ -35,14 +35,14 @@ end
 
 /- ## 修飾可能なコマンド
 `scoped` で有効範囲を限定できるコマンドには、次のようなものがあります。
-* [`elab`](./Elab.md), `elab_rules`
-* [`infix`](./Infix.md), `infixl`, `infixr`
-* [`instance`](./Instance.md)
-* [`macro`](./Macro.md), [`macro_rules`](./MacroRules.md)
-* [`notation`](./Notation.md)
-* [`postfix`](./Postfix.md)
-* [`prefix`](./Prefix.md),
-* [`syntax`](./Syntax.md)
+* [`elab`](#{root}/Declarative/Elab.md), `elab_rules`
+* [`infix`](#{root}/Declarative/Infix.md), `infixl`, `infixr`
+* [`instance`](#{root}/Declarative/Instance.md)
+* [`macro`](#{root}/Declarative/Macro.md), [`macro_rules`](#{root}/Declarative/MacroRules.md)
+* [`notation`](#{root}/Declarative/Notation.md)
+* [`postfix`](#{root}/Declarative/Postfix.md)
+* [`prefix`](#{root}/Declarative/Prefix.md),
+* [`syntax`](#{root}/Declarative/Syntax.md)
 * などなど
 
 リストの全体は、`scoped` の後に修飾できないコマンドを続けたときのエラーメッセージで確認できます。
@@ -65,7 +65,7 @@ error: <input>:1:7: expected 'binder_predicate', 'builtin_dsimproc', 'builtin_si
   run_meta parse `command "scoped def"
 
 /- ## open scoped
-`open scoped` コマンドを利用すると、特定の名前空間にある `scoped` が付けられた名前だけを有効にすることができます。単に [`open`](./Open.md) コマンドを利用するとその名前空間にあるすべての名前が有効になります。
+`open scoped` コマンドを利用すると、特定の名前空間にある `scoped` が付けられた名前だけを有効にすることができます。単に [`open`](#{root}/Declarative/Open.md) コマンドを利用するとその名前空間にあるすべての名前が有効になります。
 -/
 
 namespace Foo

booksrc/SUMMARY.md

@@ -41,21 +41,15 @@
   - [inductive: 帰納型を定義する](./Declarative/Inductive.md)
   - [infix: 中置記法](./Declarative/Infix.md)
   - [instance: インスタンスを定義する](./Declarative/Instance.md)
-  - [local: 有効範囲をセクションで限定](./Declarative/Local.md)
   - [macro_rules: 構文展開の追加](./Declarative/MacroRules.md)
   - [macro: 簡便なマクロ定義](./Declarative/Macro.md)
   - [namespace: 名前空間を宣言する](./Declarative/Namespace.md)
-  - [noncomputable: 計算不能にする](./Declarative/Noncomputable.md)
   - [notation: 記法を導入する](./Declarative/Notation.md)
   - [opaque: 簡約できない名前を宣言](./Declarative/Opaque.md)
   - [open: 名前空間を開く](./Declarative/Open.md)
-  - [partial: 再帰の停止証明をしない](./Declarative/Partial.md)
   - [postfix: 後置記法](./Declarative/Postfix.md)
   - [prefix: 前置記法](./Declarative/Prefix.md)
-  - [private: 定義を不可視にする](./Declarative/Private.md)
   - [proof_wanted: 証明を公募する](./Declarative/ProofWanted.md)
-  - [protected: フルネームを強制する](./Declarative/Protected.md)
-  - [scoped: 有効範囲を名前空間で限定](./Declarative/Scoped.md)
   - [section: 有効範囲を制限する](./Declarative/Section.md)
   - [set_option: オプション設定](./Declarative/SetOption.md)
   - [structure: 構造体を定義する](./Declarative/Structure.md)
@@ -64,6 +58,14 @@
   - [theorem: 命題を証明する](./Declarative/Theorem.md)
   - [variable: 引数を共通化する](./Declarative/Variable.md)
 
+- [修飾子](./Modifier/README.md)
+  - [local: 有効範囲をセクションで限定](./Modifier/Local.md)
+  - [noncomputable: 計算不能にする](./Modifier/Noncomputable.md)
+  - [partial: 再帰の停止証明をしない](./Modifier/Partial.md)
+  - [private: 定義を不可視にする](./Modifier/Private.md)
+  - [protected: フルネームを強制する](./Modifier/Protected.md)
+  - [scoped: 有効範囲を名前空間で限定](./Modifier/Scoped.md)
+
 - [属性](./Attribute/README.md)
   - [app_unexpander: 関数適用の表示](./Attribute/AppUnexpander.md)
   - [cases_eliminator: 独自場合分け](./Attribute/CasesEliminator.md)