Files翻訳完了 (#5)

Author: s-taiga

GLOSSARY.md

@@ -2,12 +2,14 @@
 
 | 英語 | 日本語 | 備考 |
 | --- | --- | --- |
+| abbreviation | 省略形 | |
 | annotation | 注釈 | |
 | associativity | 結合性 | |
 | attribute | 属性 | |
 | backtrack | バックトラック | 後戻りと書かれる場合あり |
 | bound variable | 束縛変数 | |
 | canonical | 標準 | |
+| carriage return | CR | |
 | case distinction | 場合分け | |
 | chapter | 章 | |
 | closed term | 閉項 | |
@@ -20,6 +22,8 @@
 | constant | 定数 | |
 | construction | 構成 | |
 | constructor | コンストラクタ | |
+| content | 内容 | |
+| context | （プログラム中のcontextの意で）コンテキスト、（文章中のcontextの意で）文脈 | |
 | core language | コア言語 | |
 | core type theory | コア型理論 | |
 | datatype | データ型 | |
@@ -29,22 +33,32 @@
 | definitional (η-)equality | 定義上の(η)等価性 | |
 | definitional proof irrelevance | 定義上の証明の無関係性 | |
 | dependent type theory | 依存型理論 | |
+| double-struck | 重ね打ち体 | |
 | effect | 作用 | |
 | elaborate | エラボレート | |
 | elaboration | エラボレーション | |
 | elaborator | エラボレータ | |
+| encoding | エンコード | |
+| English letter | 英語アルファベット | |
 | environment | 環境 | |
 | environment extensions | 環境拡張 | |
 | equational lemma | 等式の補題 | |
 | evaluate | 評価 | |
+| exclamation mark | 感嘆符 | |
 | executable | 実行ファイル | |
 | expression | 式 | |
 | formalization | 形式化 | |
+| form feed | 改ページ | |
 | functional programming language | 関数型プログラミング言語 | |
 | function extensionality | 関数外延性 | |
 | grammar | 文法 | |
+| guillemet | ギュメ | フランス語 |
+| heap region | ヒープ領域 | |
+| hierarchical identifier | 階層的識別子 | |
 | hierarchy | 階層 | |
 | identifier | 識別子 | |
+| identifier component | 識別子要素 | |
+| identifier continuation character | 識別子継続文字 | |
 | inductively-defined | 帰納的に定義された | |
 | inductive predicate | 帰納的述語 | |
 | inductive type | 帰納型 | |
@@ -61,6 +75,8 @@
 | laziness | 遅延 | |
 | language server | 言語サーバ | |
 | lemma | 補題 | |
+| letter | 文字 | |
+| letterlike | 文字様 | |
 | longest match | 最長一致 | |
 | macro | マクロ | |
 | machinery | 機構 | |
@@ -71,6 +87,7 @@
 | multi-threading | マルチスレッド | |
 | mutually inductive | 相互帰納 | |
 | namespace | 名前空間 | |
+| newline | 改行 | |
 | notation | 記法 | |
 | opaque | 不透明 | |
 | operator | 演算子 | |
@@ -86,23 +103,34 @@
 | proof state | 証明状態 | |
 | proof term | 証明項 | |
 | qualification | 修飾 | |
+| question mark | 疑問符 | |
+| quote | クォート | |
 | quotient type | 商型 | |
+| raw identifier | 生識別子 | Rust By Exampleの表現を利用 |
 | reasoning | 推論 | |
 | recovery | 回復 | |
 | recursive-descent parser | 再帰下降パーサ | |
 | reference count | 参照カウント |
+| representation | 表現 | |
+| reserved keyword | 予約キーワード | 下のreserved wordの表記ゆれかもしれないがいったん別の訳語を割り当てる |
 | reserved word | 予約語 | |
 | run-time | ランタイム | |
 | rule | ランタイム | |
 | scope | スコープ | |
+| separator | 区切り文字 | |
 | set | （数学的な集合を意味しない場合）あつまり、（数学的な集合の場合）集合 | |
 | section | 節 | |
+| serialize | シリアライズ | |
 | side effect | 副作用 | |
 | signature | シグネチャ | |
+| single quote | シングルクォート | |
 | soundness | 健全性 | |
 | specialization | 特殊化 | |
+| statement | 文 | |
 | strictness | 正格 | |
+| structure | 構造体 | |
 | subterm | 部分項 | |
+| subscript | 下付き文字 | |
 | syntactic sugar | 構文糖衣 | |
 | syntax | 構文 | |
 | syntax former | 構文形成器 | |
@@ -114,6 +142,7 @@
 | term | 項 | |
 | term elaboration | 項エラボレーション | |
 | termination | 停止 | |
+| theorem | 定理 | |
 | token | 字句 | |
 | top-level | トップレベル | |
 | transitive | 推移的 | |
@@ -122,10 +151,11 @@
 | trust | 信頼 | |
 | type class | 型クラス | |
 | type class instance synthesis | 型クラスインスタンス合成 | |
+| underscore | アンダースコア | |
 | unification | 単一化 | |
 | union | 合併 | |
 | well-founded | 整礎 | |
-| whitespace | 空白文字 | |
+| whitespace | 空白 | |
 
 
 # 英語表現をそのまま用いている単語
@@ -134,4 +164,5 @@
 | --- | --- |
 | choice node | |
 | packed array | System Verilogという言語にこの名前の文法要素がある？ |
+| prelude | |
 | subject reduction | TAPLに出てくる模様 |

Manual/Elaboration.lean

@@ -98,7 +98,7 @@ There are multiple kinds of elaboration: command elaboration implements the effe
 Tactic execution is a specialization of term elaboration.
 :::
 
-実際には、上記の段階は厳密に次々と行われるわけではありません。Lean は1つの {tech}[command] （トップレベルの宣言）をパースし、ついでエラボレートし、必要なカーネルのチェックを実行します。マクロ展開はエラボレーションの一部です；構文の一部を翻訳する前に、エラボレータはまず一番外側のレイヤに存在するマクロを展開します。マクロ構文はより深いレイヤに残っているかもしれませんが、その後でエラボレータがそれらのレイヤに到達した時に展開されます。エラボレーションには複数の種類が存在します：コマンドエラボレーションは各トップレベルのコマンドの作用（例えばデータ型の宣言・定義の保存・式の評価）を実装し、項エラボレーションは多くのコマンドで出現する項（例えばシグネチャ内の型・定義の右辺・評価される式）の構築を担当します。タクティクの実行は、項エラボレーションの特殊化です。
+実際には、上記の段階は厳密に次々と行われるわけではありません。Lean は1つの {tech}[コマンド] （command、トップレベルの宣言）をパースし、ついでエラボレートし、必要なカーネルのチェックを実行します。マクロ展開はエラボレーションの一部です；構文の一部を翻訳する前に、エラボレータはまず一番外側のレイヤに存在するマクロを展開します。マクロ構文はより深いレイヤに残っているかもしれませんが、その後でエラボレータがそれらのレイヤに到達した時に展開されます。エラボレーションには複数の種類が存在します：コマンドエラボレーションは各トップレベルのコマンドの作用（例えばデータ型の宣言・定義の保存・式の評価）を実装し、項エラボレーションは多くのコマンドで出現する項（例えばシグネチャ内の型・定義の右辺・評価される式）の構築を担当します。タクティクの実行は、項エラボレーションの特殊化です。
 
 :::comment
 When a command is elaborated, the state of Lean changes.
@@ -144,9 +144,9 @@ Based on the {lean}`SourceInfo` field, there are three relationships that {lean}
  * {lean}`SourceInfo.none` indicates no relationship to a file.
 :::
 
-成功した場合、パーサは元のソースファイルを再構築するのに十分な情報を保存します。成功しなかったパースは、パース出来なかったファイルの領域に関する情報を見逃す可能性があります。 {lean}`SourceInfo` レコード型はソースの位置と周囲の空白文字を含む、構文の一部分のソースに関する情報を記録します。 {lean}`SourceInfo` フィールドに基づいて、 {lean}`Syntax` がソースファイルに対して以下の3つの関係を持つことができます：
+成功した場合、パーサは元のソースファイルを再構築するのに十分な情報を保存します。成功しなかったパースは、パース出来なかったファイルの領域に関する情報を見逃す可能性があります。 {lean}`SourceInfo` レコード型はソースの位置と周囲の空白を含む、構文の一部分のソースに関する情報を記録します。 {lean}`SourceInfo` フィールドに基づいて、 {lean}`Syntax` がソースファイルに対して以下の3つの関係を持つことができます：
  * {lean}`SourceInfo.original` は、構文の値がパーサによって直接生成されたことを示します。
- * {lean}`SourceInfo.synthetic` は、構文の値がマクロ展開などによってプログラム的に生成されたことを示します。そうであるにも関わらず、統合的な構文は _標準_ （canonical）とマークされることがあります。これによって Lean のユーザインタフェースはこの構文をあたかもユーザが書いたかのように扱います。統合的な構文には元のファイル位置が注釈されますが、先頭や末尾の空白文字は含まれません。
+ * {lean}`SourceInfo.synthetic` は、構文の値がマクロ展開などによってプログラム的に生成されたことを示します。そうであるにも関わらず、統合的な構文は _標準_ （canonical）とマークされることがあります。これによって Lean のユーザインタフェースはこの構文をあたかもユーザが書いたかのように扱います。統合的な構文には元のファイル位置が注釈されますが、先頭や末尾の空白は含まれません。
  * {lean}`SourceInfo.none` は、ファイルとの関係がないことを示します。
 
 :::comment