翻訳準備（3回目）

GLOSSARY.md

@@ -293,6 +293,7 @@
 | underscore | アンダースコア | |
 | unification | 単一化 | |
 | union | 合併 | |
+| unit-like type | unit-like 型 | |
 | unit type | ユニット型 | |
 | universe | 宇宙 | |
 | universe level | 宇宙レベル | |

Manual.lean

@@ -170,7 +170,7 @@ file := some "the-index"
 
 翻訳に際して、機械翻訳サービス [DeepL翻訳](https://www.deepl.com/ja/translator) を参考にしました。
 
-この翻訳は原文のcommit [ade9c553a5ab008113cf33f88ced657c5146fe24](https://github.com/leanprover/reference-manual/commit/ade9c553a5ab008113cf33f88ced657c5146fe24) に基づいています。
+この翻訳は原文のcommit [27f733b339554f1cc0b3b70e9ca3054397075b97](https://github.com/leanprover/reference-manual/commit/27f733b339554f1cc0b3b70e9ca3054397075b97) に基づいています。
 
 ::::::draft
 

Manual/BasicTypes.lean

@@ -202,44 +202,94 @@ tag := "char-api-classes"
 
 {include 0 Manual.BasicTypes.String}
 
+# ユニット型（The Unit Type）
+
+:::comment
 # The Unit Type
+:::
 
+:::comment
 The unit type is the least informative type.
 It is used when a value is needed, but no further information is relevant.
 There are two varieties of the unit type:
 
+:::
+
+ユニット型は最も情報量の少ない型です。これは、値は必要だがそれ以上の情報は必要ない場合に使用されます。ユニット型には2種類あります：
+
+:::comment
  * {lean}`Unit` is a {lean}`Type` that exists in the smallest non-propositional {tech}[universe].
 
+:::
+
+ * {lean}`Unit` は {lean}`Type` であり、最小の非命題 {tech}[宇宙] に存在します。
+
+:::comment
  * {lean}`PUnit` is {tech key:="universe polymorphism"}[universe polymorphic] and can be used in any non-propositional {tech}[universe].
 
+:::
+
+ * {lean}`PUnit` は {tech}[宇宙多相] であり、任意の非命題 {tech}[宇宙] で使用することができます。
+
+:::comment
 If in doubt, use {lean}`Unit` until universe errors occur.
 
+:::
+
+悩ましい場合は、宇宙に関するエラーが発生するまでは {lean}`Unit` を使ってください。
+
 {docstring Unit}
 
 {docstring Unit.unit}
 
 {docstring PUnit}
 
+:::comment
 ## Definitional Equality
+:::
+
+## 定義上の等価性（Definitional Equality）
 
+
+:::comment
 {deftech}_Unit-like types_ are inductive types that have a single constructor which takes no non-proof parameters.
 {lean}`PUnit` is one such type.
 All elements of unit-like types are {tech key:="definitional equality"}[definitionally equal] to all other elements.
 
-:::example "Definitional Equality of {lean}`Unit`"
+:::
+
+{deftech}_unit-like 型_ （unit-like type）は非証明のパラメータを取らない単一のコンストラクタを持つ帰納型です。 {lean}`PUnit` はそのような型の1つです。unit-like 型のすべての要素は、他のすべての要素を {tech key:="定義上の等価性"}[定義上等しいです] 。
+
+:::comment
+::example "Definitional Equality of {lean}`Unit`"
+:::
+::::example "{lean}`Unit` の定義上の等価性"
+:::comment
 Every term with type {lean}`Unit` is definitionally equal to every other term with type {lean}`Unit`:
 
+:::
+
+{lean}`Unit` 型を持つすべての項は、 {lean}`Unit` 型を持つすべての項と定義上等しいです：
+
 ```lean
 example (e1 e2 : Unit) : e1 = e2 := rfl
 ```
-:::
+::::
 
-::::keepEnv
-:::example "Definitional Equality of Unit-Like Types"
+:::::keepEnv
+:::comment
+::example "Definitional Equality of Unit-Like Types"
+:::
+::::example "unit-like 型の定義上の等価性"
 
+:::comment
 Both {lean}`CustomUnit` and {lean}`AlsoUnit` are unit-like types, with a single constructor that takes no parameters.
 Every pair of terms with either type is definitionally equal.
 
+:::
+
+{lean}`CustomUnit` と {lean}`AlsoUnit` はどちらも unit-like 型であり、パラメータを取らないコンストラクタを1つ持ちます。どちらの型を持つ項のペアも定義上等しいです。
+
 ```lean
 inductive CustomUnit where
   | customUnit
@@ -251,16 +301,26 @@ structure AlsoUnit where
 example (e1 e2 : AlsoUnit) : e1 = e2 := rfl
 ```
 
+:::comment
 Types with parameters, such as {lean}`WithParam`, are also unit-like if they have a single constructor that does not take parameters.
 
+:::
+
+{lean}`WithParam` のようなパラメータを持つ型も、パラメータを取らないコンストラクタが1つあれば unit-like です。
+
 ```lean
 inductive WithParam (n : Nat) where
   | mk
 
 example (x y : WithParam 3) : x = y := rfl
 ```
 
+:::comment
 Constructors with non-proof parameters are not unit-like, even if the parameters are all unit-like types.
+:::
+
+証明ではないパラメータを持つコンストラクタは、パラメータがすべて unit-like 型であっても unit-like になりません。
+
 ```lean
 inductive NotUnitLike where
   | mk (u : Unit)
@@ -278,15 +338,20 @@ but is expected to have type
   e1 = e2 : Prop
 ```
 
+:::comment
 Constructors of unit-like types may take parameters that are proofs.
+:::
+
+unit-like 型のコンストラクタは証明であるパラメータを取ることができます。
+
 ```lean
 inductive ProofUnitLike where
   | mk : 2 = 2 → ProofUnitLike
 
 example (e1 e2 : ProofUnitLike) : e1 = e2 := rfl
 ```
-:::
 ::::
+:::::
 
 # The Empty Type
 
@@ -300,24 +365,54 @@ example (e1 e2 : ProofUnitLike) : e1 = e2 := rfl
 
 {docstring PEmpty}
 
+:::comment
 # Booleans
+:::
+
+# 真偽値（Booleans）
+
 
 {docstring Bool}
 
+:::comment
 The constructors {lean}`Bool.true` and {lean}`Bool.false` are exported from the {lean}`Bool` namespace, so they can be written {lean}`true` and {lean}`false`.
 
+:::
+
+コンストラクタ {lean}`Bool.true` と {lean}`Bool.false` は {lean}`Bool` 名前空間からエクスポートされるため、 {lean}`true` と {lean}`false` と書くことができます。
+
+:::comment
 ## Run-Time Representation
+:::
+
+## ランタイム表現（Run-Time Representation）
+
 
+:::comment
 Because {lean}`Bool` is an {tech}[enum inductive] type, it is represented by a single byte in compiled code.
 
+:::
+
+{lean}`Bool` は {tech}[列挙帰納的] 型であるため、コンパイルされたコードでは1バイトで表現されます。
+
+:::comment
 ## Booleans and Propositions
+:::
+
+## 真偽値と命題（Booleans and Propositions）
+
 
+:::comment
 Both {lean}`Bool` and {lean}`Prop` represent notions of truth.
 From a purely logical perspective, they are equivalent: {tech}[propositional extensionality] means that there are fundamentally only two propositions, namely {lean}`True` and {lean}`False`.
 However, there is an important pragmatic difference: {lean}`Bool` classifies _values_ that can be computed by programs, while {lean}`Prop` classifies statements for which code generation doesn't make sense.
 In other words, {lean}`Bool` is the notion of truth and falsehood that's appropriate for programs, while {lean}`Prop` is the notion that's appropriate for mathematics.
 Because proofs are erased from compiled programs, keeping {lean}`Bool` and {lean}`Prop` distinct makes it clear which parts of a Lean file are intended for computation.
 
+:::
+
+{lean}`Bool` と {lean}`Prop` はどちらも真理の概念を表します。純粋論理の観点から見ると、両者は同等です： {tech}[propositional extensionality] は基本的に2つの命題、すなわち {lean}`True` と {lean}`False` しか存在しないことを意味します。しかし、実用上は重要な違いがあります： {lean}`Bool` はプログラムで計算できる _値_ を分類し、 {lean}`Prop` はコード生成が意味を為さない文を分類します。言い換えると、 {lean}`Bool` はプログラムに適した真偽の概念であり、 {lean}`Prop` は数学に適した概念です。コンパイルされたプログラムから証明は消去されるため、 {lean}`Bool` と {lean}`Prop` を区別しておくことで Lean ファイルのどの部分が計算を目的としているかが明確になります。
+
 ```lean (show := false)
 section BoolProp
 
@@ -332,29 +427,49 @@ example : (true = true) = True := by simp
 #check decide
 ```
 
+:::comment
 A {lean}`Bool` can be used wherever a {lean}`Prop` is expected.
 There is a {tech}[coercion] from every {lean}`Bool` {lean}`b` to the proposition {lean}`b = true`.
 By {lean}`propext`, {lean}`true = true` is equal to {lean}`True`, and {lean}`false = true` is equal to {lean}`False`.
 
+:::
+
+{lean}`Bool` は {lean}`Prop` が期待されているところではどこでも使うことができます。すべての {lean}`Bool` {lean}`b` から命題 {lean}`b = true` への {tech}[coercion] が存在します。 {lean}`propext` により、 {lean}`true = true` は {lean}`True` に、 {lean}`false = true` は {lean}`False` にそれぞれ等しいです。
+
+:::comment
 Not every proposition can be used by programs to make run-time decisions.
 Otherwise, a program could branch on whether the Collatz conjecture is true or false!
 Many propositions, however, can be checked algorithmically.
 These propositions are called {tech}_decidable_ propositions, and have instances of the {lean}`Decidable` type class.
 The function {name}`Decidable.decide` converts a proof-carrying {lean}`Decidable` result into a {lean}`Bool`.
 This function is also a coercion from decidable propositions to {lean}`Bool`, so {lean}`(2 = 2 : Bool)` evaluates to {lean}`true`.
 
+:::
+
+全ての命題をプログラムがランタイム時の判断に使えるわけではありません。そうでなければコラッツ予想が真か偽かでプログラムが分岐してしまいます！しかし、多くの命題はアルゴリズムでチェックすることができます。これらの命題は {tech}_決定可能_ な命題と呼ばれ、 {lean}`Decidable` 型クラスを持ちます。関数 {name}`Decidable.decide` は証明を格納した {lean}`Decidable` の結果を {lean}`Bool` に変換します。この関数は決定可能な命題から {lean}`Bool` への強制演算でもあるため、 {lean}`(2 = 2 : Bool)` は {lean}`true` と評価されます。
+
 ```lean (show := false)
 /-- info: true -/
 #guard_msgs in
 #eval (2 = 2 : Bool)
 end BoolProp
 ```
 
+:::comment
 ## Syntax
+:::
+
+## 構文（Syntax）
 
-:::syntax term
+
+::::syntax term
+:::comment
 The infix operators `&&`, `||`, and `^^` are notations for {lean}`Bool.and`, {lean}`Bool.or`, and {lean}`Bool.xor`, respectively.
 
+:::
+
+中置演算子 `&&` ・ `||` ・ `^^` はそれぞれ {lean}`Bool.and` ・ {lean}`Bool.or` ・ {lean}`Bool.xor` の表記です。
+
 ```grammar
 $_:term && $_:term
 ```
@@ -364,30 +479,50 @@ $_:term || $_:term
 ```grammar
 $_:term ^^ $_:term
 ```
-:::
+::::
 
-:::syntax term
+::::syntax term
+:::comment
 The prefix operator `!` is notation for {lean}`Bool.not`.
+:::
+
+前置演算子 `!` は {lean}`Bool.not` の表記です。
+
 ```grammar
 !$_:term
 ```
-:::
+::::
 
 
+:::comment
 ## API Reference
+:::
 
+## API リファレンス（API Reference）
+
+
+:::comment
 ### Logical Operations
+:::
+
+### 論理演算子（Logical Operations）
+
 
 ```lean (show := false)
 section ShortCircuit
 
 axiom BIG_EXPENSIVE_COMPUTATION : Bool
 ```
 
+:::comment
 The functions {name}`cond`, {name Bool.and}`and`, and {name Bool.or}`or` are short-circuiting.
 In other words, {lean}`false && BIG_EXPENSIVE_COMPUTATION` does not need to execute {lean}`BIG_EXPENSIVE_COMPUTATION` before returning `false`.
 These functions are defined using the {attr}`macro_inline` attribute, which causes the compiler to replace calls to them with their definitions while generating code, and the definitions use nested pattern matching to achieve the short-circuiting behavior.
 
+:::
+
+関数 {name}`cond` ・ {name Bool.and}`and` ・ {name Bool.or}`or` は短絡します。つまり、 {lean}`false && BIG_EXPENSIVE_COMPUTATION` は `false` を返す前に {lean}`BIG_EXPENSIVE_COMPUTATION` を実行する必要はありません。これらの関数は {attr}`macro_inline` 属性を使用して定義されています。これによりコンパイラはコードを生成する際に関数の呼び出しを定義に置き換え、入れ子のパターンマッチを用いる定義が短絡評価されるようになります。
+
 ```lean (show := false)
 end ShortCircuit
 ```
@@ -405,11 +540,21 @@ end ShortCircuit
 
 {docstring Bool.atLeastTwo}
 
+:::comment
 ### Comparisons
+:::
+
+### 比較（Comparisons）
+
 
 {docstring Bool.decEq}
 
+:::comment
 ### Conversions
+:::
+
+### 変換（Conversions）
+
 
 {docstring Bool.toISize}
 

Manual/Classes/BasicClasses.lean

@@ -56,13 +56,13 @@ Lean の型クラスの多くは、加算や配列インデックスのような
 
 :::comment
 # Decidability
-%%%
-tag := "decidable-propositions"
-%%%
 
 :::
 
 # 決定可能性（Decidability）
+%%%
+tag := "decidable-propositions"
+%%%
 
 :::comment
 A proposition is {deftech}_decidable_ if it can be checked algorithmically.{index}[decidable]{index subterm:="decidable"}[proposition]

Manual/Elaboration.lean

@@ -431,7 +431,7 @@ To provide a uniform interface to functions defined via structural and well-foun
 In the function's namespace, `eq_unfold` relates the function directly to its definition, `eq_def` relates it to the definition after instantiating implicit parameters, and $`N` lemmas `eq_N` relate each case of its pattern-matching to the corresponding right-hand side, including sufficient assumptions to indicate that earlier branches were not taken.
 :::
 
-構造的に単純な再帰関数の場合、その翻訳は型の再帰子を使用します。このような関数はカーネルで実行すると比較的効率的である傾向があり、定義された等式が定義上成立し、理解も容易です。型の再帰子で捕捉できないその他のパターンの再帰を使用する関数は {deftech}[整礎再帰] （well-founded recursion）を使用して翻訳されます。これは各再帰呼び出しのたびに何かしらの基準が減少することの証明のもとの構造的な再帰です。Lean はこれらのケースの多くを自動的に導出できますが、手作業での証明が必要なものもあります。整礎再帰はより柔軟なものですが、基準が減少することを示す証明項が定義する等式が成立するのは命題上だけであるため、結果として得られる関数はカーネルでの実行速度が遅くなることが多いです。構造的で整礎な再帰によって定義された関数に統一されたインタフェースを提供し、それ自身の正しさをチェックするために、エラボレータは関数をもとの定義に関連付ける等式の補題を証明します。関数の名前空間において、`eq_unfold` は関数を直接定義に関連付け、`eq_def` は暗黙のパラメータをインスタンス化した後の定義に関連付け、 $`N` 個の補題 `eq_N` はパターンマッチの各ケースと対応する右辺を関連付けます。これにはそれより前の分岐が取られないことの十分な仮定を含みます。
+構造的に単純な再帰関数の場合、その翻訳は型の再帰子を使用します。このような関数はカーネルで実行すると比較的効率的である傾向があり、定義された等式が定義上成立し、理解も容易です。型の再帰子で捕捉できないその他のパターンの再帰を使用する関数は {deftech}[整礎再帰] （well-founded recursion）を使用して翻訳されます。これは各再帰呼び出しのたびに何かしらの {deftech}_測度_ （measure）が減少することの証明のもとの構造的な再帰です。Lean はこれらのケースの多くを自動的に導出できますが、手作業での証明が必要なものもあります。整礎再帰はより柔軟なものですが、基準が減少することを示す証明項が定義する等式が成立するのは命題上だけであるため、結果として得られる関数はカーネルでの実行速度が遅くなることが多いです。構造的で整礎な再帰によって定義された関数に統一されたインタフェースを提供し、それ自身の正しさをチェックするために、エラボレータは関数をもとの定義に関連付ける等式の補題を証明します。関数の名前空間において、`eq_unfold` は関数を直接定義に関連付け、`eq_def` は暗黙のパラメータをインスタンス化した後の定義に関連付け、 $`N` 個の補題 `eq_N` はパターンマッチの各ケースと対応する右辺を関連付けます。これにはそれより前の分岐が取られないことの十分な仮定を含みます。
 
 :::::keepEnv
 :::comment

Manual/IO.lean

@@ -32,7 +32,7 @@ tag := "io"
 
 
 Lean is a pure functional programming language.
-While Lean code is strictly evaluated at run time, the order of evaluation that is used during type checking, especially while checking {tech}[definitional equality], is formally unspecified and makes use of a number of heuristics that improve performance but are subject to change.
+While Lean code is strictly evaluated at run time, the order of evaluation that is used during type checking, especially while checking {tech}[定義上の等価性]definitional equality, is formally unspecified and makes use of a number of heuristics that improve performance but are subject to change.
 This means that simply adding operations that perform side effects (such as file I/O, exceptions, or mutable references) would lead to programs in which the order of effects is unspecified.
 During type checking, even terms with free variables are reduced; this would make side effects even more difficult to predict.
 Finally, a basic principle of Lean's logic is that functions are _functions_ that map each element of the domain to a unique element of the range.
@@ -129,7 +129,7 @@ example : BaseIO = EIO Empty := rfl
 ## Errors and Error Handling
 
 Error handling in the {lean}`IO` monad uses the same facilities as any other {tech}[exception monad].
-In particular, throwing and catching exceptions uses the methods of the {name}`MonadExceptOf` {tech}[type class].
+In particular, throwing and catching exceptions uses the methods of the {name}`MonadExceptOf` {tech}[型クラス]type class.
 The exceptions thrown in {lean}`IO` have the type {lean}`IO.Error`.
 The constructors of this type represent the low-level errors that occur on most operating systems, such as files not existing.
 The most-used constructor is {name IO.Error.userError}`userError`, which covers all other cases and includes a string that describes the problem.