06_macros

GROSSARY.md

@@ -21,6 +21,7 @@
 | implication | 含意 |
 | instantiation | インスタンス化 |
 | kind | 種 |
+| macro hygiene | マクロの健全性 |
 | metavariable | メタ変数 |
 | notation | 記法 |
 | parse | パース |
@@ -44,5 +45,5 @@
 
 | 用語 |
 | --- |
-| macro hygiene |
 | loose |
+| syntax quotation |

lean/main/05_syntax.lean

@@ -532,7 +532,7 @@ Lets go through the definition one constructor at a time:
 - `missing` は Lean のコンパイラによってパースできないようなものがある際に使われます。このおかげで Lean はファイルの一部で構文エラーがあっても、そこから回復してファイルの残りの部分を理解しようとします。これはまた、このコンストラクタはあまり気にされないものであるということでもあります。
 - `node` は名前の通り、構文木のノードです。ノードは `kind : SyntaxNodeKind` と呼ばれるものを持っています。この `SyntaxNodeKind` はただの `Lean.Name` です。基本的に、各 `syntax` 宣言は自動的に生成された `SyntaxNodeKind` を受け取り（この名前は `syntax (name := foo) ... : cat` で明示的に指定することもできます）、これによって Lean に「この関数は特定の構文構築を行う責任がある」ということを伝えます。さらに、木の中の全てのノードと同様に、この関数にも子があり、この場合は `Array Syntax` をいう形式をとっています。
 - `atom` は（1つを除いて）階層の一番下にあるすべての構文オブジェクトを表します。例えば、上の演算子 ` ⊕ ` と ` LXOR ` は atom として表現されます。
-- `ident` は `atom` で前述したこのルールの例外です。`ident` と `atom` の違いは実に明白です：識別子はそれを表すにあたって `String` の代わりに `Lean.Name` を持ちます。なぜ `Lean.Name` が単なる `String` ではないのかはマクロの章で詳しく説明する macro hygiene と呼ばれる概念に関連しています。今のところ、これらは基本的に等価であると考えることができます。
+- `ident` は `atom` で前述したこのルールの例外です。`ident` と `atom` の違いは実に明白です：識別子はそれを表すにあたって `String` の代わりに `Lean.Name` を持ちます。なぜ `Lean.Name` が単なる `String` ではないのかはマクロの章で詳しく説明するマクロの健全性（macro hygiene）と呼ばれる概念に関連しています。今のところ、これらは基本的に等価であると考えることができます。
 
 --#--
 ### Constructing new `Syntax`