From b58f488770cf91c37b4fc1377bfa7d3cdf6a8b02 Mon Sep 17 00:00:00 2001 From: s-taiga Date: Mon, 2 Dec 2024 22:48:59 +0900 Subject: [PATCH 1/2] =?UTF-8?q?=E7=BF=BB=E8=A8=B3=E9=96=8B=E5=A7=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Manual/Language/Classes/BasicClasses.lean | 3 +++ Manual/Language/Classes/DerivingHandlers.lean | 3 +++ 2 files changed, 6 insertions(+) diff --git a/Manual/Language/Classes/BasicClasses.lean b/Manual/Language/Classes/BasicClasses.lean index f9b369d..7dcbb36 100644 --- a/Manual/Language/Classes/BasicClasses.lean +++ b/Manual/Language/Classes/BasicClasses.lean @@ -13,7 +13,10 @@ open Manual open Verso.Genre open Verso.Genre.Manual +/- #doc (Manual) "Basic Classes" => +-/ +#doc (Manual) "基本的なクラス（Basic Classes）" => %%% tag := "basic-classes" %%% diff --git a/Manual/Language/Classes/DerivingHandlers.lean b/Manual/Language/Classes/DerivingHandlers.lean index 8d10d00..9880908 100644 --- a/Manual/Language/Classes/DerivingHandlers.lean +++ b/Manual/Language/Classes/DerivingHandlers.lean @@ -40,7 +40,10 @@ 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" %%% From 116695160e26c25ec63f3d8bd831b7e213c1e577 Mon Sep 17 00:00:00 2001 From: s-taiga Date: Tue, 3 Dec 2024 23:14:49 +0900 Subject: [PATCH 2/2] =?UTF-8?q?=E7=BF=BB=E8=A8=B3=E5=AE=8C=E4=BA=86?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- GLOSSARY.md | 1 + Manual/Language/Classes/BasicClasses.lean | 45 +++++++++++++++++++ Manual/Language/Classes/DerivingHandlers.lean | 36 +++++++++++++-- 3 files changed, 78 insertions(+), 4 deletions(-) diff --git a/GLOSSARY.md b/GLOSSARY.md index 469fe36..d325b72 100644 --- a/GLOSSARY.md +++ b/GLOSSARY.md @@ -298,6 +298,7 @@ | choice node | | | cumulative | | | impredicativity, predicativity | | +| inhabited | | | no confusion | | | out, semi-out | | | packed array | System Verilogという言語にこの名前の文法要素がある？ | diff --git a/Manual/Language/Classes/BasicClasses.lean b/Manual/Language/Classes/BasicClasses.lean index 7dcbb36..956ae32 100644 --- a/Manual/Language/Classes/BasicClasses.lean +++ b/Manual/Language/Classes/BasicClasses.lean @@ -21,40 +21,70 @@ open Verso.Genre.Manual 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 +::: + +# 決定可能性（Decidability） + {docstring Decidable} {docstring DecidableRel} {docstring DecidableEq} +:::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 @@ -67,8 +97,13 @@ Many Lean type classes exist in order to allow built-in notations such as additi {docstring ToString} +:::comment # Arithmetic and Bitwise Operators +::: + +# 算術・ビット演算子（Arithmetic and Bitwise Operators） + {docstring Zero} {docstring NeZero} @@ -119,14 +154,24 @@ Many Lean type classes exist in order to allow built-in notations such as additi {docstring HXor} +:::comment # Append +::: + +# 結合（Append） + {docstring HAppend} {docstring Append} +:::comment # Data Lookups +::: + +# データの検索（Data Lookups） + {docstring GetElem} {docstring GetElem?} diff --git a/Manual/Language/Classes/DerivingHandlers.lean b/Manual/Language/Classes/DerivingHandlers.lean index 9880908..7b03f15 100644 --- a/Manual/Language/Classes/DerivingHandlers.lean +++ b/Manual/Language/Classes/DerivingHandlers.lean @@ -43,11 +43,12 @@ def derivableClassList : DirectiveExpander /- #doc (Manual) "Deriving Handlers" => -/ -#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`. @@ -55,16 +56,33 @@ When a user requests that an instance of a class be derived, its registered hand 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 @@ -74,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 @@ -93,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 @@ -132,5 +160,5 @@ def deriveIsEnum (declNames : Array Name) : CommandElabM Bool := do initialize registerDerivingHandler ``IsEnum deriveIsEnum ``` -::: :::: +:::::