04_metam (#5)

* 翻訳開始

* 翻訳完了

* 表現微修正

Author: s-taiga

GROSSARY.md

@@ -3,25 +3,34 @@
 | 英語 | 日本語 |
 | --- | --- |
 | abstract syntax tree | 抽象構文木 |
+| assign | 割当 |
 | binder | 束縛子 |
 | bound variable | 束縛変数 |
 | concrete syntax tree | 解析木 |
 | context | コンテキスト（証明やプログラム中のスコープを指す場合）、文脈（それ以外） |
 | delaboration | デラボレーション |
+| definitionally equal | 定義上等しい |
 | elaborate | 精緻化 |
 | elaboration | エラボレーション |
 | elaborator | エラボレータ |
 | free variable | 自由変数 |
+| full normalisation | 完全正規化 |
 | hypothesis | 仮定 |
 | expression | 式 |
+| implementation detail | 実装の詳細 |
 | implication | 含意 |
+| instantiation | インスタンス化 |
+| kind | 種 |
 | metavariable | メタ変数 |
 | notation | 記法 |
 | parse | パース |
+| proof term | 証明項 |
 | reduction | 簡約 |
 | reflection | リフレクション |
 | syntax | 構文 |
+| target type | ターゲットの型 |
 | term | 項（式を構成する要素）、用語 |
+| transparency | 透過度 |
 | unification | ユニフィケーション |
 | universe | 宇宙 |
 | universe-polymorphic constant | 宇宙多相な定数 |

book.toml

@@ -3,7 +3,7 @@ authors = ["Arthur Paulino, Damiano Testa, Edward Ayers, Evgenia Karunus, Henrik
 language = "ja"
 multilingual = false
 src = "md"
-title = "Metaprogramming in Lean 4"
+title = "Metaprogramming in Lean 4 日本語訳"
 
 [output.html]
 git-repository-url = "https://github.com/lean-ja/lean4-metaprogramming-book-ja"