BasicClasses_DerivingHandlers翻訳 (#18)

* 翻訳開始

* 翻訳完了

Author: s-taiga

GLOSSARY.md

@@ -261,6 +261,7 @@
 | term | 項 | |
 | term elaboration | 項エラボレーション | |
 | termination | 停止 | |
+| The Law of the Excluded Middle | 排中律 | |
 | theorem | 定理 | |
 | token | 字句 | |
 | top-level | トップレベル | |
@@ -298,6 +299,7 @@
 | choice node | |
 | cumulative | |
 | impredicativity, predicativity | |
+| inhabited | |
 | no confusion | |
 | out, semi-out | |
 | packed array | System Verilogという言語にこの名前の文法要素がある？ |

Manual/Classes/BasicClasses.lean

@@ -13,38 +13,66 @@ open Manual
 open Verso.Genre
 open Verso.Genre.Manual
 
+/-
 #doc (Manual) "Basic Classes" =>
+-/
+#doc (Manual) "基本的なクラス（Basic Classes）" =>
 %%%
 tag := "basic-classes"
 %%%
 
+:::comment
 Many Lean type classes exist in order to allow built-in notations such as addition or array indexing to be overloaded.
 
+:::
+
+Lean の型クラスの多くは、加算や配列インデックスのような組み込み記法をオーバーロードできるようにするために存在します。
+
+:::comment
 # Boolean Equality Tests
 
+:::
+
+# 真偽値上の等価性のテスト（Boolean Equality Tests）
+
 {docstring BEq}
 
 {docstring Hashable}
 
 {docstring LawfulBEq}
 
+:::comment
 # Ordering
 
+:::
+
+# 順序（Ordering）
+
 {docstring Ord}
 
 {docstring LT}
 
 {docstring LE}
 
+:::comment
 # Decidability
 %%%
 tag := "decidable-propositions"
 %%%
 
+:::
+
+# 決定可能性（Decidability）
+
+:::comment
 A proposition is {deftech}_decidable_ if it can be checked algorithmically.{index}[decidable]{index subterm:="decidable"}[proposition]
 The Law of the Excluded Middle means that every proposition is true or false, but it provides no way to check which of the two cases holds, which can often be useful.
 By default, only algorithmic {lean}`Decidable` instances for which code can be generated are in scope; opening the `Classical` namespace makes every proposition decidable.
 
+:::
+
+アルゴリズム的にチェック可能である命題は {deftech}_決定可能_ （decidable）であると言います。 {index}[decidable]{index subterm:="decidable"}[proposition] 排中律は、すべての命題が真か偽であることを意味しますが、2つのケースのどちらが成り立つかをチェックする方法は提供しません。デフォルトでは、コードを生成できるアルゴリズム的な {lean}`Decidable` インスタンスのみがスコープに含まれます；`Classical` 名前空間を開くと、すべての命題が決定可能になります。
+
 {docstring Decidable}
 
 {docstring DecidableRel}
@@ -55,9 +83,17 @@ By default, only algorithmic {lean}`Decidable` instances for which code can be g
 
 {docstring Decidable.byCases}
 
-::::keepEnv
-:::example "Excluded Middle and {lean}`Decidable`"
+:::::keepEnv
+:::comment
+::example "Excluded Middle and {lean}`Decidable`"
+:::
+::::example "排中律と {lean}`Decidable`"
+:::comment
 The equality of functions from {lean}`Nat` to {lean}`Nat` is not decidable:
+:::
+
+{lean}`Nat` から {lean}`Nat` への関数の等価性は決定不可能です：
+
 ```lean (error:=true) (name := NatFunNotDecEq)
 example (f g : Nat → Nat) : Decidable (f = g) := inferInstance
 ```
@@ -67,24 +103,39 @@ failed to synthesize
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 ```
 
+:::comment
 Opening `Classical` makes every proposition decidable; however, declarations and examples that use this fact must be marked {keywordOf Lean.Parser.Command.declaration}`noncomputable` to indicate that code should not be generated for them.
+:::
+
+`Classical` を開くと、すえｂての命題が決定可能になります；しかし、この事実を使用する宣言と例には、コードを生成すべきでないことを示すために {keywordOf Lean.Parser.Command.declaration}`noncomputable` とマークしなければなりません。
+
 ```lean
 open Classical
 noncomputable example (f g : Nat → Nat) : Decidable (f = g) := inferInstance
 ```
 
-:::
 ::::
+:::::
 
 
+:::comment
 # Inhabited Types
 
+:::
+
+# inhabited な型（Inhabited Types）
+
 {docstring Inhabited}
 
 {docstring Nonempty}
 
+:::comment
 # Visible Representations
 
+:::
+
+# 表現の可視化（Visible Representations）
+
 :::planned 135
 
  * How to write a correct {name}`Repr` instance
@@ -97,8 +148,13 @@ noncomputable example (f g : Nat → Nat) : Decidable (f = g) := inferInstance
 
 {docstring ToString}
 
+:::comment
 # Arithmetic and Bitwise Operators
 
+:::
+
+# 算術・ビット演算子（Arithmetic and Bitwise Operators）
+
 {docstring Zero}
 
 {docstring NeZero}
@@ -149,14 +205,24 @@ noncomputable example (f g : Nat → Nat) : Decidable (f = g) := inferInstance
 
 {docstring HXor}
 
+:::comment
 # Append
 
+:::
+
+# 結合（Append）
+
 {docstring HAppend}
 
 {docstring Append}
 
+:::comment
 # Data Lookups
 
+:::
+
+# データの検索（Data Lookups）
+
 {docstring GetElem}
 
 {docstring GetElem?}

Manual/Classes/DerivingHandlers.lean

@@ -40,28 +40,49 @@ def derivableClassList : DirectiveExpander
     let theList ← `(Verso.Doc.Block.ul #[$[⟨0, #[Verso.Doc.Block.para #[$itemStx]]⟩],*])
     return #[theList]
 
+/-
 #doc (Manual) "Deriving Handlers" =>
+-/
+#doc (Manual) "導出ハンドラ（Deriving Handlers）" =>
 %%%
 tag := "deriving-handlers"
 %%%
 
+:::comment
 Instance deriving uses a table of {deftech}_deriving handlers_ that maps type class names to metaprograms that derive instances for them.
 Deriving handlers may be added to the table using {lean}`registerDerivingHandler`, which should be called in an {keywordOf Lean.Parser.Command.initialize}`initialize` block.
 Each deriving handler should have the type {lean}`Array Name → CommandElabM Bool`.
 When a user requests that an instance of a class be derived, its registered handlers are called one at a time.
 They are provided with all of the names in the mutual block for which the instance is to be derived, and should either correctly derive an instance and return {lean}`true` or have no effect and return {lean}`false`.
 When a handler returns {lean}`true`, no further handlers are called.
 
+:::
+
+インスタンスの導出は {deftech}_導出ハンドラ_ （deriving handler）のテーブルを使用し、型クラス名をインスタンスを導出するメタプログラムにマッピングします。導出ハンドラは {lean}`registerDerivingHandler` を使用してテーブルに追加することができます。これは {keywordOf Lean.Parser.Command.initialize}`initialize` ブロック内で呼び出す必要があります。それぞれの導出ハンドラは {lean}`Array Name → CommandElabM Bool` 型を持つ必要があります。ユーザがクラスのインスタンス導出を要求すると、登録されているハンドラが1つずつ呼び出されます。これらのハンドラにはインスタンスを導出させる相互ブロック内のすべての名前が提供され、正しくインスタンスを導出した場合は {lean}`true` を、そうでない場合は何もせずに {lean}`false` を返します。ハンドラが {lean}`true` を返すと、それ以降のハンドラは呼び出されません。
+
+:::comment
 Lean includes deriving handlers for the following classes:
+:::
+
+Lean には以下のクラスの導出ハンドラがあります：
+
 :::derivableClassList
 :::
 
 {docstring Lean.Elab.registerDerivingHandler}
 
 
-::::keepEnv
-:::example "Deriving Handlers"
+:::::keepEnv
+:::comment
+::example "Deriving Handlers"
+:::
+::::example "導出ハンドラ"
+:::comment
 Instances of the {name}`IsEnum` class demonstrate that a type is a finite enumeration by providing a bijection between the type and a suitably-sized {name}`Fin`:
+:::
+
+{name}`IsEnum` クラスのインスタンスは型に対して適切なサイズの {name}`Fin` との間に全単射を提供することによって型が有限に列挙されることを示します：
+
 ```lean
 class IsEnum (α : Type) where
   size : Nat
@@ -71,8 +92,13 @@ class IsEnum (α : Type) where
   from_to_id : ∀ (x : α), fromIdx (toIdx x) = x
 ```
 
+:::comment
 For inductive types that are trivial enumerations, where no constructor expects any parameters, instances of this class are quite repetitive.
 The instance for `Bool` is typical:
+:::
+
+帰納型は自明な列挙であり、コンストラクタがパラメータを期待しない帰納型ではこのクラスのインスタンスにおいては非常に繰り返しが多いコードになります。 `Bool` のインスタンスが典型的です：
+
 ```lean
 instance : IsEnum Bool where
   size := 2
@@ -90,7 +116,12 @@ instance : IsEnum Bool where
     | true => rfl
 ```
 
+:::comment
 The deriving handler programmatically constructs each pattern case, by analogy to the {lean}`IsEnum Bool` implementation:
+:::
+
+導出ハンドラは {lean}`IsEnum Bool` の実装をなぞるようにそれぞれのパターンのケースをプログラムで構築します：
+
 ```lean
 open Lean Elab Parser Term Command
 
@@ -129,5 +160,5 @@ def deriveIsEnum (declNames : Array Name) : CommandElabM Bool := do
 initialize
   registerDerivingHandler ``IsEnum deriveIsEnum
 ```
-:::
 ::::
+:::::