Elaboration翻訳

GLOSSARY.md

@@ -2,37 +2,136 @@
 
 | 英語 | 日本語 | 備考 |
 | --- | --- | --- |
-| core type theory | 中核となる型理論 | |
+| annotation | 注釈 | |
+| associativity | 結合性 | |
+| attribute | 属性 | |
+| backtrack | バックトラック | 後戻りと書かれる場合あり |
+| bound variable | 束縛変数 | |
+| canonical | 標準 | |
+| case distinction | 場合分け | |
+| chapter | 章 | |
+| closed term | 閉項 | |
+| combinator | コンビネータ | |
 | command | コマンド | |
+| command elaboration | コマンドエラボレーション | |
+| compilation | コンパイル | |
+| completion | 補完 | |
+| consistency | 一貫性 | |
 | constant | 定数 | |
+| construction | 構成 | |
+| constructor | コンストラクタ | |
+| core language | コア言語 | |
+| core type theory | コア型理論 | |
+| datatype | データ型 | |
+| debugging trace | デバッグトレース | |
+| declaration | 宣言 | |
 | definition | 定義 | |
+| definitional (η-)equality | 定義上の(η)等価性 | |
+| definitional proof irrelevance | 定義上の証明の無関係性 | |
 | dependent type theory | 依存型理論 | |
+| effect | 作用 | |
+| elaborate | エラボレート | |
+| elaboration | エラボレーション | |
 | elaborator | エラボレータ | |
+| environment | 環境 | |
+| environment extensions | 環境拡張 | |
+| equational lemma | 等式の補題 | |
+| evaluate | 評価 | |
+| executable | 実行ファイル | |
+| expression | 式 | |
 | formalization | 形式化 | |
 | functional programming language | 関数型プログラミング言語 | |
+| function extensionality | 関数外延性 | |
+| grammar | 文法 | |
+| hierarchy | 階層 | |
+| identifier | 識別子 | |
+| inductively-defined | 帰納的に定義された | |
 | inductive predicate | 帰納的述語 | |
 | inductive type | 帰納型 | |
+| info tree | 情報木 | |
+| initialization | 初期化 | |
+| instantiate | インスタンス化 | |
 | interactive theorem prover | 対話型定理証明器 | |
+| interface | インタフェース | |
+| interleave | 交互に実行する | |
+| intermediate representation | 中間表現 | |
 | kernel | カーネル | |
+| keyword | キーワード | |
+| kind | 種 | |
+| laziness | 遅延 | |
 | language server | 言語サーバ | |
+| lemma | 補題 | |
+| longest match | 最長一致 | |
+| macro | マクロ | |
+| machinery | 機構 | |
+| macro Expansion | マクロ展開 | |
+| mapping | マッピング | |
+| memoization | メモ化 | |
 | monad | モナド | |
 | multi-threading | マルチスレッド | |
-| notation | 記法 |
+| mutually inductive | 相互帰納 | |
+| namespace | 名前空間 | |
+| notation | 記法 | |
+| opaque | 不透明 | |
+| operator | 演算子 | |
+| open scope | 開いたスコープ | |
+| packrat parse | パックラットパース | 一般的にはパックラット構文解析と呼ばれることが多いが、parseをパースと書くことに合わせた |
+| parse | パース | |
+| parser | パーサ | |
+| pattern matching | パターンマッチ | |
+| precedence | 優先順位 | 構文解析・演算子等の優先具合を指す |
+| pretty printer | プリティプリンタ | |
+| primitive | プリミティブ | |
 | proof checker | 証明チェッカ | |
 | proof state | 証明状態 | |
 | proof term | 証明項 | |
+| qualification | 修飾 | |
+| quotient type | 商型 | |
+| reasoning | 推論 | |
+| recovery | 回復 | |
+| recursive-descent parser | 再帰下降パーサ | |
 | reference count | 参照カウント |
+| reserved word | 予約語 | |
 | run-time | ランタイム | |
+| rule | ランタイム | |
+| scope | スコープ | |
+| set | （数学的な集合を意味しない場合）あつまり、（数学的な集合の場合）集合 | |
+| section | 節 | |
+| side effect | 副作用 | |
+| signature | シグネチャ | |
 | soundness | 健全性 | |
+| specialization | 特殊化 | |
+| strictness | 正格 | |
+| subterm | 部分項 | |
+| syntactic sugar | 構文糖衣 | |
 | syntax | 構文 | |
 | syntax former | 構文形成器 | |
+| syntax trees | 構文木 | |
+| syntax value | 構文の値 | |
+| synthetic syntax | 統合的な構文 | |
 | tactic | タクティク | |
 | Technical Terminology | 専門用語 | |
+| term | 項 | |
+| term elaboration | 項エラボレーション | |
+| termination | 停止 | |
+| token | 字句 | |
+| top-level | トップレベル | |
+| transitive | 推移的 | |
+| transitivity | 推移性 | |
+| tree | 木 | |
 | trust | 信頼 | |
+| type class | 型クラス | |
+| type class instance synthesis | 型クラスインスタンス合成 | |
+| unification | 単一化 | |
+| union | 合併 | |
+| well-founded | 整礎 | |
+| whitespace | 空白文字 | |
 
 
 # 英語表現をそのまま用いている単語
 
 | 用語 | 備考 |
 | --- | --- |
-| packed array | 日本語訳が見つからなかったため。System Verilogという言語にこの名前の文法要素がある？ |
+| choice node | |
+| packed array | System Verilogという言語にこの名前の文法要素がある？ |
+| subject reduction | TAPLに出てくる模様 |