Simp翻訳 (#14)

* 翻訳開始

* 翻訳完了

GLOSSARY.md

@@ -37,6 +37,8 @@
 | command elaboration | コマンドエラボレーション | |
 | compilation | コンパイル | |
 | completion | 補完 | |
+| confluence | 合流性 | |
+| conjunction | 連言 | |
 | consistency | 一貫性 | |
 | constant | 定数 | |
 | construction | 構成 | |
@@ -76,6 +78,7 @@
 | environment | 環境 | |
 | environment extensions | 環境拡張 | |
 | equational lemma | 等式の補題 | |
+| equivalence | 同値性 | |
 | equivalent | 同値 | |
 | evaluate | 評価 | |
 | evidence | 根拠 | |
@@ -162,6 +165,7 @@
 | nested | ネストされた | |
 | newline | 改行 | |
 | non-dependent | 非依存的 | |
+| normal form | 正規形 | |
 | notation | 記法 | |
 | opaque | 不透明 | |
 | operator | 演算子 | |
@@ -178,6 +182,7 @@
 | pretty printer | プリティプリンタ | |
 | primitive | プリミティブ | |
 | primitive recursion | 原始再帰 | |
+| procedure | 手続き | |
 | product type | 直積型 | |
 | projection function | 射影関数 | |
 | proof checker | 証明チェッカ | |
@@ -200,6 +205,7 @@
 | representation | 表現 | |
 | reserved keyword | 予約キーワード | 下のreserved wordの表記ゆれかもしれないがいったん別の訳語を割り当てる |
 | reserved word | 予約語 | |
+| rewrite | 書き換え | |
 | run-length encoding | 連長圧縮 | |
 | run-time | ランタイム | |
 | rule | 規則 | |
@@ -208,12 +214,15 @@
 | scope | スコープ | |
 | scrutinee | 被検査対象 | |
 | separator | 区切り文字 | |
-| set | （数学的な集合を意味しない場合）あつまり、（数学的な集合の場合）集合 | |
+| set | （数学的な集合の場合）集合、（数学的な集合を意味しない場合でプログラミング上実体のある集まりの場合）セット、（それ以外）あつまり | |
 | section | 節 | |
 | serialize | シリアライズ | |
 | shadow | （変数の隠蔽の意で）シャドーイング | |
 | side effect | 副作用 | |
 | signature | シグネチャ | |
+| simplifier | 単純化器 | |
+| simplify | 単純化 | |
+| simp set | simp セット | |
 | single quote | シングルクォート | |
 | singleton | 単集合 | |
 | soundness | 健全性 | |

Manual/Elaboration.lean

@@ -210,7 +210,7 @@ Term elaboration may modify all of these fields except the open scopes.
 Additionally, it has access to all the machinery needed to create fully-explicit terms in the core language from Lean's terse, friendly syntax, including unification, type class instance synthesis, and type checking.
 :::
 
-コマンドエラボレーションと項エラボレーションは異なる能力を持ちます。コマンドエラボレーションは環境に副作用を与える可能性があり、 {lean}`IO` で任意の計算を実行するアクセス権を持っています。Lean の環境は名前から定義への通常のマッピングに加え、 {deftech}[環境拡張] （environment extension）で定義される追加データを含んでいます；環境拡張は {tactic}`simp` 補題・カスタムのプリティプリンタ・コンパイラの中間表現などの内部を含む、Lean コードに関する他のほとんどの情報を追跡するために使用されます。コマンドエラボレーションはまた、コンパイラの情報出力・警告・およびエラー内容を含むメッセージログ・メタデータをもとの構文に関連付ける {tech}[情報木] のあつまり（証明状態の表示・識別子の補完・ドキュメントの表示などの対話的な機能に使用されます）・蓄積されたデバッグトレース・開いた {tech}[scope] ・マクロ展開に関連するいくつかの内部状態を維持します。項エラボレーションは開いたスコープを除くこれらすべてのフィールドを変更することができます。さらに、Lean の簡潔で親しみやすい構文からコア言語で完全に明示的な項を作成するために必要な単一化・型クラスインスタンス合成・型チェックを含むすべての機構にアクセスすることができます。
+コマンドエラボレーションと項エラボレーションは異なる能力を持ちます。コマンドエラボレーションは環境に副作用を与える可能性があり、 {lean}`IO` で任意の計算を実行するアクセス権を持っています。Lean の環境は名前から定義への通常のマッピングに加え、 {deftech}[環境拡張] （environment extension）で定義される追加データを含んでいます；環境拡張は {tactic}`simp` 補題・カスタムのプリティプリンタ・コンパイラの中間表現などの内部を含む、Lean コードに関する他のほとんどの情報を追跡するために使用されます。コマンドエラボレーションはまた、コンパイラの情報出力・警告・およびエラー内容を含むメッセージログ・メタデータをもとの構文に関連付ける {tech}[情報木] のセット（証明状態の表示・識別子の補完・ドキュメントの表示などの対話的な機能に使用されます）・蓄積されたデバッグトレース・開いた {tech}[scope] ・マクロ展開に関連するいくつかの内部状態を維持します。項エラボレーションは開いたスコープを除くこれらすべてのフィールドを変更することができます。さらに、Lean の簡潔で親しみやすい構文からコア言語で完全に明示的な項を作成するために必要な単一化・型クラスインスタンス合成・型チェックを含むすべての機構にアクセスすることができます。
 
 :::comment
 The first step in both term and command elaboration is macro expansion.
@@ -232,7 +232,7 @@ Command elaborators accept syntax and return no value, but may have monadic side
 While both term and command elaborators have access to {lean}`IO`, it's unusual that they perform side effects; exceptions include interactions with external tools or solvers.
 :::
 
-マクロ展開の後、項とコマンドエラボレータのどちらも、構文の種をエラボレータの処理にマップするテーブルを参照します。項エラボレータは、構文とオプションで期待される型を、前述の非常に機能的なモナドを使用するコア言語の式にマッピングします。コマンドエラボレータは構文を受け入れ、値を返しませんが、グローバルのコマンド状態に対してモナドの副作用を持つかもしれません。項とコマンドエラボレータのどちらも {lean}`IO` にアクセスできますが、副作用を実行するのは一般的ではありません；例外は外部ツールやソルバとのやり取りを含みます。
+マクロ展開の後、項とコマンドエラボレータのどちらも、構文の種をエラボレータの手続きにマップするテーブルを参照します。項エラボレータは、構文とオプションで期待される型を、前述の非常に機能的なモナドを使用するコア言語の式にマッピングします。コマンドエラボレータは構文を受け入れ、値を返しませんが、グローバルのコマンド状態に対してモナドの副作用を持つかもしれません。項とコマンドエラボレータのどちらも {lean}`IO` にアクセスできますが、副作用を実行するのは一般的ではありません；例外は外部ツールやソルバとのやり取りを含みます。
 
 :::comment
 The elaborator tables may be extended to enable the use of new syntax for both terms and commands by extending the tables.

Manual/Intro.lean

@@ -17,7 +17,7 @@ set_option pp.rawOnError true
 /-
 #doc (Manual) "Introduction" =>
 -/
-#doc (Manual) "はじめに" =>
+#doc (Manual) "はじめに（Introduction）" =>
 %%%
 htmlSplit := .never
 %%%
@@ -71,7 +71,7 @@ Lean のプログラムは新しいタクティクや証明の自動化を実装
 ## History
 :::
 
-## 歴史
+## 歴史（History）
 
 :::comment
 Leonardo de Moura launched the Lean project when he was at Microsoft Research in 2013, and Lean 0.1 was officially released on June 16, 2014.
@@ -115,7 +115,7 @@ Leonardo de Moura と彼の共同設立者である Sebastian Ullrich は2023年
 # Typographical Conventions
 :::
 
-# 表記ルール
+# 表記規則（Typographical Conventions）
 
 :::comment
 This document makes use of a number of typographical and layout conventions to indicate various aspects of the information being presented.
@@ -127,7 +127,7 @@ This document makes use of a number of typographical and layout conventions to i
 ## Lean Code
 :::
 
-## Lean のコード
+## Lean のコード（Lean Code）
 
 :::comment
 This document contains many Lean code examples.
@@ -234,7 +234,7 @@ Identifiers in code examples are hyperlinked to their documentation.
 ## Examples
 :::
 
-## 例
+## 例（Examples）
 
 :::comment
 Illustrative examples are in callout boxes, as below:
@@ -271,7 +271,7 @@ inductive Even : Nat → Prop where
 ## Technical Terminology
 :::
 
-## 専門用語
+## 専門用語（Technical Terminology）
 
 :::comment
 {deftech}_Technical terminology_ refers to terms used in a very specific sense when writing technical material, such as this reference.
@@ -284,7 +284,7 @@ Uses of {tech}[technical terminology] are frequently hyperlinked to their defini
 ## Constant, Syntax, and Tactic References
 :::
 
-## 定数・構文・タクティクの参照
+## 定数・構文・タクティクの参照（Constant, Syntax, and Tactic References）
 
 :::comment
 Definitions, inductive types, syntax formers, and tactics have specific descriptions.

Manual/Language.lean

@@ -44,7 +44,7 @@ Only well-typed terms have a meaning.
 
 :::
 
-{deftech}_項_ （term）は {deftech}_式_ （expression）としても知られ、Lean のコア言語における意味の基本単位です。これらは {tech}[エラボレータ] によってユーザが書いた構文から生成されます。Lean の型システムは項をその _型_ （type）に関連付けます。型は集合を表し、項は集合の個々の要素を表すと考えることができます。Lean の型理論のルールに従った型を持つ項は {deftech}_well-typed_ と言います。well-typed である項のみが意味を持ちます。
+{deftech}_項_ （term）は {deftech}_式_ （expression）としても知られ、Lean のコア言語における意味の基本単位です。これらは {tech}[エラボレータ] によってユーザが書いた構文から生成されます。Lean の型システムは項をその _型_ （type）に関連付けます。型は集合を表し、項は集合の個々の要素を表すと考えることができます。Lean の型理論の規則に従った型を持つ項は {deftech}_well-typed_ と言います。well-typed である項のみが意味を持ちます。
 
 :::comment
 Terms are a dependently typed λ-calculus: they include function abstraction, application, variables, and `let`-bindings.

Manual/Language/Files.lean

@@ -218,7 +218,7 @@ These keywords must also be quoted with guillemets to be used as identifier comp
 Contexts in which keywords may be used as identifiers without guillemets, such as constructor names in inductive datatypes, are {deftech}_raw identifier_ contexts.{index (subterm:="raw")}[identifier]
 :::
 
-識別子要素として予約キーワードを使うことがあるかもしれません。予約キーワードの特定のあつまりは、アクティブな構文拡張のあつまりに依存し、またそれらはインポートされたモジュールと現在開いている名前空間のあつまりに依存するかもしれません；Lean はこれを列挙することができません。これらのキーワードはほとんどの構文で識別子の構成要素として使用するために、ギュメでクォートする必要があります。帰納的データ型のコンストラクタ名など、キーワードをギュメなしで識別子として使用できるコンテキストは {deftech}_生識別子_ （raw identifier）コンテキストです。 {index (subterm:="raw")}[identifier]
+識別子要素として予約キーワードを使うことがあるかもしれません。予約キーワードの特定のセットは、アクティブな構文拡張のセットに依存し、またそれらはインポートされたモジュールと現在開いている名前空間のセットに依存するかもしれません；Lean はこれを列挙することができません。これらのキーワードはほとんどの構文で識別子の構成要素として使用するために、ギュメでクォートする必要があります。帰納的データ型のコンストラクタ名など、キーワードをギュメなしで識別子として使用できるコンテキストは {deftech}_生識別子_ （raw identifier）コンテキストです。 {index (subterm:="raw")}[identifier]
 
 :::comment
 Identifiers that contain one or more `'.'` characters, and thus consist of more than one identifier component, are called {deftech}[hierarchical identifiers].
@@ -308,7 +308,7 @@ Modules do not necessarily correspond to namespaces.
 Modules may add names to any namespace, and importing a module has no effect on the set of currently open namespaces.
 :::
 
-モジュールは必ずしも名前空間に対応するとは限りません。モジュールはどの名前空間にも名前を追加することができ、モジュールをインポートしても現在開いている名前空間のあつまりには影響しません。
+モジュールは必ずしも名前空間に対応するとは限りません。モジュールはどの名前空間にも名前を追加することができ、モジュールをインポートしても現在開いている名前空間のセットには影響しません。
 
 :::comment
 The imported module name is translated to a filename by replacing dots (`'.'`) in its name with directory separators.