| 英語 | 日本語 |
|---|---|
| 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 | 種 |
| macro hygiene | マクロの健全性 |
| metavariable | メタ変数 |
| notation | 記法 |
| parse | パース |
| precedence | 優先順位 |
| pretty print | プリティプリント |
| priority | 優先度 |
| proof term | 証明項 |
| reduction | 簡約 |
| reflection | リフレクション |
| syntactically | 構文的 |
| syntax | 構文 |
| syntax category | 構文カテゴリ |
| target type | ターゲットの型 |
| term | 項(式を構成する要素)、用語 |
| transparency | 透過度 |
| unification | ユニフィケーション |
| universe | 宇宙 |
| universe-polymorphic constant | 宇宙多相な定数 |
| β-reduction | β簡約 |
| 用語 |
|---|
| loose |
| parenthesizer |
| syntax quotation |
| synthetic metavariable |
| unexpander |