From 3d0a80af83f3ba86097a225956a4d25649123068 Mon Sep 17 00:00:00 2001 From: s-taiga Date: Sun, 24 Nov 2024 17:50:07 +0900 Subject: [PATCH] =?UTF-8?q?=E7=BF=BB=E8=A8=B3=E6=BA=96=E5=82=99=E5=AE=8C?= =?UTF-8?q?=E4=BA=86=EF=BC=882=E5=9B=9E=E7=9B=AE=EF=BC=89?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- GLOSSARY.md | 1 + Manual.lean | 2 +- Manual/BasicTypes.lean | 36 ++--- Manual/BasicTypes/Nat.lean | 114 ++++++------- Manual/BasicTypes/String.lean | 84 +++++----- Manual/BasicTypes/String/Literals.lean | 18 +-- Manual/Elaboration.lean | 10 +- Manual/Language.lean | 2 +- Manual/Language/Classes.lean | 4 +- Manual/Language/Files.lean | 4 +- Manual/Language/Functions.lean | 30 ++-- Manual/Language/InductiveTypes.lean | 94 +++++------ .../Language/InductiveTypes/LogicalModel.lean | 22 +-- .../Language/InductiveTypes/Structures.lean | 20 +-- Manual/NotationsMacros.lean | 4 +- Manual/NotationsMacros/Notations.lean | 4 +- Manual/NotationsMacros/Operators.lean | 2 +- Manual/NotationsMacros/SyntaxDef.lean | 2 +- Manual/Simp.lean | 46 +++--- Manual/Tactics.lean | 150 +++++++++++------- Manual/Tactics/Conv.lean | 48 +++--- Manual/Tactics/Custom.lean | 18 +-- Manual/Tactics/Reference.lean | 128 +++++++-------- 23 files changed, 436 insertions(+), 407 deletions(-) diff --git a/GLOSSARY.md b/GLOSSARY.md index feac9d0..eebdabc 100644 --- a/GLOSSARY.md +++ b/GLOSSARY.md @@ -37,6 +37,7 @@ | command elaboration | コマンドエラボレーション | | | compilation | コンパイル | | | completion | 補完 | | +| configuration item | 設定項目 | | | confluence | 合流性 | | | conjunction | 連言 | | | consistency | 一貫性 | | diff --git a/Manual.lean b/Manual.lean index 95f2461..60364a9 100644 --- a/Manual.lean +++ b/Manual.lean @@ -168,7 +168,7 @@ file := some "the-index" 翻訳に際して、機械翻訳サービス [DeepL翻訳](https://www.deepl.com/ja/translator) を参考にしました。 -この翻訳は原文のcommit [2fbf58d9210323e4ebc0a002d9f761074da462cf](https://github.com/leanprover/reference-manual/commit/2fbf58d9210323e4ebc0a002d9f761074da462cf) に基づいています。 +この翻訳は原文のcommit [ade9c553a5ab008113cf33f88ced657c5146fe24](https://github.com/leanprover/reference-manual/commit/ade9c553a5ab008113cf33f88ced657c5146fe24) に基づいています。 ::::::draft diff --git a/Manual/BasicTypes.lean b/Manual/BasicTypes.lean index d56c5ee..e3a03d9 100644 --- a/Manual/BasicTypes.lean +++ b/Manual/BasicTypes.lean @@ -85,47 +85,47 @@ tag := "Float" :::comment # Characters +::: + +# 文字（Characters） %%% tag := "Char" %%% -::: - -# 文字（Characters） {docstring Char} :::comment ## Syntax +::: + +## 構文（Syntax） %%% tag := "char-syntax" %%% -::: - -## 構文（Syntax） :::comment ## Logical Model +::: + +## 論理モデル（Logical Model） %%% tag := "char-model" %%% -::: - -## 論理モデル（Logical Model） :::comment ## Run-Time Representation +::: + +## ランタイム表現（Run-Time Representation） %%% tag := "char-runtime" %%% -::: - -## ランタイム表現（Run-Time Representation） :::comment In monomorphic contexts, characters are represented as 32-bit immediate values. In other words, a field of a constructor or structure of type `Char` does not require indirection to access. In polymorphic contexts, characters are boxed. @@ -137,25 +137,25 @@ In monomorphic contexts, characters are represented as 32-bit immediate values. :::comment ## API Reference +::: + +## API リファレンス（API Reference） %%% tag := "char-api" %%% -::: - -## API リファレンス（API Reference） :::comment ### Character Classes +::: + +### 文字クラス（Character Classes） %%% tag := "char-api-classes" %%% -::: - -### 文字クラス（Character Classes） {docstring Char.isAlpha} diff --git a/Manual/BasicTypes/Nat.lean b/Manual/BasicTypes/Nat.lean index 4ecd4f2..8aaf2ff 100644 --- a/Manual/BasicTypes/Nat.lean +++ b/Manual/BasicTypes/Nat.lean @@ -38,14 +38,14 @@ Because the natural numbers are fundamental to both mathematical reasoning and p :::comment # Logical Model +::: + +# 論理モデル（Logical Model） %%% tag := "nat-model" %%% -::: - -# 論理モデル（Logical Model） {docstring Nat} @@ -101,14 +101,14 @@ Look up and document :::comment ## Performance Notes +::: + +## パフォーマンスについての注記（Performance Notes） %%% tag := "nat-performance" %%% -::: - -## パフォーマンスについての注記（Performance Notes） :::comment Using Lean's built-in arithmetic operators, rather than redefining them, is essential. @@ -122,14 +122,14 @@ While defining arithmetic from scratch can be a useful learning exercise, these :::comment # Syntax +::: + +# 構文（Syntax） %%% tag := "nat-syntax" %%% -::: - -# 構文（Syntax） :::comment Natural number literals are overridden using the {lean}`OfNat` type class. @@ -145,24 +145,24 @@ Document this elsewhere, insert a cross-reference here :::comment # API Reference +::: + +# API リファレンス（API Reference） %%% tag := "nat-api" %%% -::: - -# API リファレンス（API Reference） :::comment ## Arithmetic +::: + +## 算術（Arithmetic） %%% tag := "nat-api-arithmetic" %%% -::: - -## 算術（Arithmetic） {docstring Nat.pred} @@ -184,13 +184,13 @@ tag := "nat-api-arithmetic" :::comment ### Bitwise Operations +::: + +### ビット演算（Bitwise Operations） %%% tag := "nat-api-bitwise" %%% -::: - -### ビット演算（Bitwise Operations） {docstring Nat.shiftLeft} @@ -208,14 +208,14 @@ tag := "nat-api-bitwise" :::comment ## Minimum and Maximum +::: + +## 最小・最大（Minimum and Maximum） %%% tag := "nat-api-minmax" %%% -::: - -## 最小・最大（Minimum and Maximum） {docstring Nat.min} @@ -225,14 +225,14 @@ tag := "nat-api-minmax" :::comment ## GCD and LCM +::: + +## 最大公約数と最小公倍数（GCD and LCM） %%% tag := "nat-api-gcd-lcm" %%% -::: - -## 最大公約数と最小公倍数（GCD and LCM） {docstring Nat.gcd} @@ -240,14 +240,14 @@ tag := "nat-api-gcd-lcm" :::comment ## Powers of Two +::: + +## 2の累乗（Powers of Two） %%% tag := "nat-api-pow2" %%% -::: - -## 2の累乗（Powers of Two） {docstring Nat.isPowerOfTwo} @@ -255,25 +255,25 @@ tag := "nat-api-pow2" :::comment ## Comparisons +::: + +## 比較（Comparisons） %%% tag := "nat-api-comparison" %%% -::: - -## 比較（Comparisons） :::comment ### Boolean Comparisons +::: + +### 真偽値の比較（Boolean Comparisons） %%% tag := "nat-api-comparison-bool" %%% -::: - -### 真偽値の比較（Boolean Comparisons） {docstring Nat.beq} @@ -283,13 +283,13 @@ tag := "nat-api-comparison-bool" :::comment ### Decidable Equality +::: + +### 決定的な等価性（Decidable Equality） %%% tag := "nat-api-deceq" %%% -::: - -### 決定的な等価性（Decidable Equality） {docstring Nat.decEq} @@ -299,13 +299,13 @@ tag := "nat-api-deceq" :::comment ### Predicates +::: + +### 述語（Predicates） %%% tag := "nat-api-predicates" %%% -::: - -### 述語（Predicates） {docstring Nat.le} @@ -315,13 +315,13 @@ tag := "nat-api-predicates" :::comment ## Iteration +::: + +## 反復（Iteration） %%% tag := "nat-api-iteration" %%% -::: - -## 反復（Iteration） :::comment Many iteration operators come in two versions: a structurally recursive version and a tail-recursive version. @@ -363,13 +363,13 @@ The structurally recursive version is typically easier to use in contexts where :::comment ## Conversion +::: + +## 変換（Conversion） %%% tag := "nat-api-conversion" %%% -::: - -## 変換（Conversion） {docstring Nat.toUInt8} @@ -407,13 +407,13 @@ tag := "nat-api-conversion" :::comment ### Metaprogramming and Internals +::: + +### メタプログラミングと内部（Metaprogramming and Internals） %%% tag := "nat-api-meta" %%% -::: - -### メタプログラミングと内部（Metaprogramming and Internals） {docstring Nat.fromExpr?} @@ -421,14 +421,14 @@ tag := "nat-api-meta" :::comment ## Casts +::: + +## キャスト（Casts） %%% tag := "nat-api-cast" %%% -::: - -## キャスト（Casts） {docstring NatCast} @@ -436,14 +436,14 @@ tag := "nat-api-cast" :::comment ## Elimination +::: + +## 除去（Elimination） %%% tag := "nat-api-elim" %%% -::: - -## 除去（Elimination） :::comment The recursion principle that is automatically generated for {lean}`Nat` results in proof goals that are phrased in terms of {lean}`Nat.zero` and {lean}`Nat.succ`. @@ -475,14 +475,14 @@ Insert reference to section on how to do this :::comment ### Alternative Induction Principles +::: + +### 代替の帰納原理（Alternative Induction Principles） %%% tag := "nat-api-induction" %%% -::: - -### 代替の帰納原理（Alternative Induction Principles） {docstring Nat.strongInductionOn} diff --git a/Manual/BasicTypes/String.lean b/Manual/BasicTypes/String.lean index e3c8d6a..c9b831b 100644 --- a/Manual/BasicTypes/String.lean +++ b/Manual/BasicTypes/String.lean @@ -133,14 +133,14 @@ Lean ランタイムの多くの文字列関数は、おぷじぇくとヘッダ :::comment ## Performance Notes +::: + +## パフォーマンスについての注記（Performance Notes） %%% tag := "string-performance" %%% -::: - -## パフォーマンスについての注記（Performance Notes） :::comment Despite the fact that they appear to be an ordinary constructor and projection, {name}`String.mk` and {name}`String.data` take *time linear in the length of the string*. @@ -153,25 +153,25 @@ This is because they must implement the conversions between lists of characters {include 0 Manual.BasicTypes.String.Literals} # API リファレンス（API Reference） - -:::comment -# API Reference %%% tag := "string-api" %%% + +:::comment +# API Reference ::: :::comment ## Constructing +::: + +## 構成（Constructing） %%% tag := "string-api-build" %%% -::: - -## 構成（Constructing） {docstring String.singleton} @@ -183,14 +183,14 @@ tag := "string-api-build" :::comment ## Conversions +::: + +## 変換（Conversions） %%% tag := "string-api-convert" %%% -::: - -## 変換（Conversions） {docstring String.toList} @@ -210,13 +210,13 @@ tag := "string-api-convert" :::comment ## Properties +::: + +## プロパティ（Properties） %%% tag := "string-api-props" %%% -::: - -## プロパティ（Properties） {docstring String.isEmpty} @@ -226,13 +226,13 @@ tag := "string-api-props" :::comment ## Positions +::: + +## 位置（Positions） %%% tag := "string-api-pos" %%% -::: - -## 位置（Positions） {docstring String.Pos} @@ -256,13 +256,13 @@ tag := "string-api-pos" :::comment ## Lookups and Modifications +::: + +## 検索と変更（Lookups and Modifications） %%% tag := "string-api-lookup" %%% -::: - -## 検索と変更（Lookups and Modifications） {docstring String.get} @@ -325,13 +325,13 @@ tag := "string-api-lookup" :::comment ## Folds and Aggregation +::: + +## 畳み込みと集約（Folds and Aggregation） %%% tag := "string-api-fold" %%% -::: - -## 畳み込みと集約（Folds and Aggregation） {docstring String.map} @@ -345,13 +345,13 @@ tag := "string-api-fold" :::comment ## Comparisons +::: + +## 比較（Comparisons） %%% tag := "string-api-compare" %%% -::: - -## 比較（Comparisons） {docstring String.le} @@ -371,13 +371,13 @@ tag := "string-api-compare" :::comment ## Manipulation +::: + +## 操作（Manipulation） %%% tag := "string-api-modify" %%% -::: - -## 操作（Manipulation） {docstring String.split} @@ -452,13 +452,13 @@ Clients are responsible for checking whether they've reached the beginning or en :::comment ## Substrings +::: + +## 部分文字列（Substrings） %%% tag := "string-api-substring" %%% -::: - -## 部分文字列（Substrings） :::TODO Substring API xref @@ -470,14 +470,14 @@ Substring API xref :::comment ## Proof Automation +::: + +## 証明自動化（Proof Automation） %%% tag := "string-simp" %%% -::: - -## 証明自動化（Proof Automation） {docstring String.reduceGT} @@ -505,14 +505,14 @@ tag := "string-simp" :::comment ## Metaprogramming +::: + +## メタプログラミング（Metaprogramming） %%% tag := "string-api-meta" %%% -::: - -## メタプログラミング（Metaprogramming） {docstring String.toName} @@ -524,14 +524,14 @@ tag := "string-api-meta" :::comment ## Encodings +::: + +## エンコード（Encodings） %%% tag := "string-api-encoding" %%% -::: - -## エンコード（Encodings） {docstring String.utf16PosToCodepointPos} diff --git a/Manual/BasicTypes/String/Literals.lean b/Manual/BasicTypes/String/Literals.lean index a604a55..f2a5dd6 100644 --- a/Manual/BasicTypes/String/Literals.lean +++ b/Manual/BasicTypes/String/Literals.lean @@ -31,13 +31,13 @@ Lean には3種類の文字列リテラルがあります：通常の文字列 :::comment # String Literals +::: + +# 文字列リテラル（String Literals） %%% tag := "string-literals" %%% -::: - -# 文字列リテラル（String Literals） :::comment String literals begin and end with a double-quote character `"`. {index subterm:="string"}[literal] @@ -131,13 +131,13 @@ The parser error is: :::comment # Interpolated Strings +::: + +# 補間文字列（Interpolated Strings） %%% tag := "string-interpolation" %%% -::: - -# 補間文字列（Interpolated Strings） :::comment Preceding a string literal with `s!` causes it to be processed as an {deftech}[_interpolated string_], in which regions of the string surrounded by `{` and `}` characters are parsed and interpreted as Lean expressions. @@ -166,13 +166,13 @@ Preceding a literal with `m!` causes the interpolation to result in an instance :::comment # Raw String Literals +::: + +# 生文字列リテラル %%% tag := "raw-string-literals" %%% -::: - -# 生文字列リテラル :::comment In {deftech}[raw string literals], {index subterm:="raw string"}[literal] there are no escape sequences or gaps, and each character denotes itself exactly. diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean index d29e95f..866f36c 100644 --- a/Manual/Elaboration.lean +++ b/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、トップレベルの宣言）をパースし、ついでエラボレートし、必要なカーネルのチェックを実行します。マクロ展開はエラボレーションの一部です；構文の一部を翻訳する前に、エラボレータはまず一番外側のレイヤに存在するマクロを展開します。マクロ構文はより深いレイヤに残っているかもしれませんが、その後でエラボレータがそれらのレイヤに到達した時に展開されます。エラボレーションには複数の種類が存在します：コマンドエラボレーションは各トップレベルのコマンドの作用（例えば {tech}[帰納型] の宣言・定義の保存・式の評価）を実装し、項エラボレーションは多くのコマンドで出現する項（例えばシグネチャ内の型・定義の右辺・評価される式）の構築を担当します。タクティクの実行は、項エラボレーションの特殊化です。 :::comment When a command is elaborated, the state of Lean changes. @@ -196,7 +196,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}[section scope] ・マクロ展開に関連するいくつかの内部状態を維持します。項エラボレーションは開いたスコープを除くこれらすべてのフィールドを変更することができます。さらに、Lean の簡潔で親しみやすい構文からコア言語で完全に明示的な項を作成するために必要な単一化・型クラスインスタンス合成・型チェックを含むすべての機構にアクセスすることができます。 :::comment The first step in both term and command elaboration is macro expansion. @@ -218,7 +218,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. @@ -296,7 +296,7 @@ The language implemented by the kernel is a version of the Calculus of Construct カーネルが実装する言語は Calculus of Constructions の一種で、以下の特徴を持つ依存型理論です： + 完全な依存型 -+ 相互に帰納的であったり、他の帰納的データ型の下で入れ子になった再帰を含んだりする帰納的に定義されたデータ型 ++ 相互に帰納的であったり、他の帰納型の下で入れ子になった再帰を含んだりする帰納的に定義されたデータ型 + {tech}[impredicative] ・定義上証明と irrelevant な {tech}[命題] の拡張的 {tech}[宇宙] + {tech}[predicative] なデータの宇宙の非蓄積な階層 * 定義上の計算規則を伴った {ref "quotients"}[商型] （Quotient type） @@ -427,7 +427,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）を使用して翻訳されます。これは各再帰呼び出しのたびに何かしらの基準が減少することの証明のもとの構造的な再帰です。Lean はこれらのケースの多くを自動的に導出できますが、手作業での証明が必要なものもあります。整礎再帰はより柔軟なものですが、基準が減少することを示す証明項が定義する等式が成立するのは命題上だけであるため、結果として得られる関数はカーネルでの実行速度が遅くなることが多いです。構造的で整礎な再帰によって定義された関数に統一されたインタフェースを提供し、それ自身の正しさをチェックするために、エラボレータは関数をもとの定義に関連付ける等式の補題を証明します。関数の名前空間において、`eq_unfold` は関数を直接定義に関連付け、`eq_def` は暗黙のパラメータをインスタンス化した後の定義に関連付け、 $`N` 個の補題 `eq_N` はパターンマッチの各ケースと対応する右辺を関連付けます。これにはそれより前の分岐が取られないことの十分な仮定を含みます。 :::::keepEnv :::comment diff --git a/Manual/Language.lean b/Manual/Language.lean index fb07956..2a367ce 100644 --- a/Manual/Language.lean +++ b/Manual/Language.lean @@ -1001,7 +1001,7 @@ The {keywordOf Lean.Parser.Command.declaration}`instance` command is described i ::: -これらのコマンドはすべて Lean によってシグネチャに応じた項へ {tech key:="エラボレータ"}[エラボレート] されます。結果を破棄する {syntaxKind}`example` を除き、Lean のコア言語での結果の式は将来の環境で使用するために保存されます。 +これらのコマンドはすべて Lean によってシグネチャに応じた項へ {tech key:="エラボレータ"}[エラボレート] されます。結果を破棄する {syntaxKind}`example` を除き、Lean のコア言語での結果の式は将来の環境で使用するために保存されます。 {keywordOf Lean.Parser.Command.declaration}`instance` コマンドについては {ref "instance-declarations"}[インスタンス宣言の節] で記述します。 :::syntax Lean.Parser.Command.declaration ```grammar diff --git a/Manual/Language/Classes.lean b/Manual/Language/Classes.lean index f9526b6..9712330 100644 --- a/Manual/Language/Classes.lean +++ b/Manual/Language/Classes.lean @@ -41,7 +41,7 @@ tag := "type-classes" An operation is _polymorphic_ if it can be used with multiple types. In Lean, polymorphism comes in three varieties: - 1. {tech}[universe polymorphism], where the sorts in a definition can be instantiated in various ways, + 1. {tech}[宇宙多相]universe polymorphism, where the sorts in a definition can be instantiated in various ways, 2. functions that take types as (potentially implicit) parameters, allowing a single body of code to work with any type, and 3. {deftech}_ad-hoc polymorphism_, implemented with type classes, in which operations to be overloaded may have different implementations for different types. @@ -314,7 +314,7 @@ tag := "class inductive" Most type classes follow the paradigm of a set of overloaded methods from which clients may choose freely. This is naturally modeled by a product type, from which the overloaded methods are projections. Some classes, however, are sum types: they require that the recipient of the synthesized instance first check _which_ of the available instance constructors was provided. -To account for these classes, a class declaration may consist of an arbitrary {tech}[inductive type], not just an extended form of structure declaration. +To account for these classes, a class declaration may consist of an arbitrary {tech}[帰納型]inductive type, not just an extended form of structure declaration. :::syntax Lean.Parser.Command.declaration ```grammar diff --git a/Manual/Language/Files.lean b/Manual/Language/Files.lean index 33f6b10..ba68c56 100644 --- a/Manual/Language/Files.lean +++ b/Manual/Language/Files.lean @@ -24,7 +24,7 @@ Modules correspond to source files, and are imported into other modules based on In other words, the names and folder structures of files are significant in Lean code. ::: -Lean におけるコンパイルの最小単位は1つの {deftech}[モジュール] （module）です。モジュールはソースファイルに対応し、ファイル名に基づいて他のモジュールにインポートされます。言い換えれば、Lean コードではファイルの名前とフォルダ構造が重要です。 +Lean におけるコンパイルの最小単位は1つの {deftech key:="module"}[モジュール] （module）です。モジュールはソースファイルに対応し、ファイル名に基づいて他のモジュールにインポートされます。言い換えれば、Lean コードではファイルの名前とフォルダ構造が重要です。 :::comment # Modules @@ -154,7 +154,7 @@ tag := "keywords-and-identifiers" An {tech}[identifier] consists of one or more identifier components, separated by `'.'`.{index}[identifier] ::: -{tech}[識別子] （identifier）は `'.'` 区切りで1つ以上の識別子要素から構成されます。 {index}[identifier] +{tech}[identifier] は `'.'` 区切りで1つ以上の識別子要素から構成されます。 {index}[identifier] :::comment {deftech}[Identifier components] consist of a letter or letter-like character or an underscore (`'_'`), followed by zero or more identifier continuation characters. diff --git a/Manual/Language/Functions.lean b/Manual/Language/Functions.lean index 2be4ab4..990fdc5 100644 --- a/Manual/Language/Functions.lean +++ b/Manual/Language/Functions.lean @@ -189,14 +189,14 @@ i : Nat :::comment # Functions +::: + +# 関数（Functions） %%% tag := "function-terms" %%% -::: - -# 関数（Functions） :::comment Terms with function types can be created via abstractions, introduced with the {keywordOf Lean.Parser.Term.fun}`fun` keyword. @@ -243,14 +243,14 @@ However, not all functions originate from abstractions: {tech}[type constructors :::comment # Currying +::: + +# カリー化（Currying） %%% tag := "currying" %%% -::: - -# カリー化（Currying） :::comment In Lean's core type theory, every function maps each element of the domain to a single element of the range. @@ -309,14 +309,14 @@ These are equivalent to writing nested {keywordOf Lean.Parser.Term.fun}`fun` ter :::comment # Implicit Functions +::: + +# 暗黙の関数（Implicit Functions） %%% tag := "implicit-functions" %%% -::: - -# 暗黙の関数（Implicit Functions） :::comment Lean supports implicit parameters to functions. @@ -619,14 +619,14 @@ fun n => :::comment # Extensionality +::: + +# 外延性（Extensionality） %%% tag := "function-extensionality" %%% -::: - -# 外延性（Extensionality） :::comment Definitional equality of functions in Lean is {deftech}_intensional_. @@ -675,14 +675,14 @@ When reasoning about functions, the theorem {lean}`funext`{margin}[Unlike some i :::comment # Totality and Termination +::: + +# 全域性と停止（Totality and Termination） %%% tag := "totality" %%% -::: - -# 全域性と停止（Totality and Termination） :::comment Functions can be defined recursively using {keywordOf Lean.Parser.Command.declaration}`def`. diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean index b8c5547..9a47aa5 100644 --- a/Manual/Language/InductiveTypes.lean +++ b/Manual/Language/InductiveTypes.lean @@ -45,7 +45,7 @@ Lean additionally produces a number of helper constructions based on the recurso ::: -帰納型の型コンストラクタとコンストラクタに基づいて、Lean は {deftech}_再帰子_{index}[recursor]{see "recursor"}[eliminator] （recursor）を導出します。論理的には、再帰子は帰納原理や除去則を表し、計算上は原始再帰計算を表します。再帰関数の停止は、再帰子の使用に変換することで正当化されるため、Lean のカーネルは再帰子の適用の型チェックを行うだけでよく、停止性の分析を別途行う必要はありません。Lean はさらに、システムの他の場所でも使用される再帰子 {margin}[_再帰子_ という用語は再帰的でないデータ型でも常に使用されます。] に基づいた数多くの補助的な構成を提供しています。 +帰納型の型コンストラクタとコンストラクタに基づいて、Lean は {deftech}_再帰子_{index}[recursor]{see "recursor"}[eliminator] （recursor）を導出します。論理的には、再帰子は帰納原理や除去則を表し、計算上は原始再帰計算を表します。再帰関数の停止は、再帰子の使用に変換することで正当化されるため、Lean のカーネルは再帰子の適用の型チェックを行うだけでよく、停止性の分析を別途行う必要はありません。Lean はさらに、システムの他の場所でも使用される再帰子 {margin}[_再帰子_ という用語は再帰的でない型でも常に使用されます。] に基づいた数多くの補助的な構成を提供しています。 :::comment _Structures_ are a special case of inductive types that have exactly one constructor. @@ -64,13 +64,13 @@ This section describes the specific details of the syntax used to specify both i :::comment # Inductive Type Declarations +::: + +# 帰納型の宣言 %%% tag := "inductive-declarations" %%% -::: - -# 帰納型の宣言 ::::syntax command (alias := «inductive») ```grammar @@ -119,7 +119,7 @@ If no signature is provided, then the constructor's type is inferred by insertin ::: -コンストラクタの仕様は {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`where` の後に続きます。コンストラクタは必須ではありません。コンストラクタのないデータ型としては {lean}`False` と {lean}`Empty` などがまさに当てはまります。各コンストラクタの指定は、縦棒（`'|'`、Unicode `'VERTICAL BAR' (U+007c)`）・宣言修飾子・名前で始まります。名前は {tech}[生識別子] です。宣言シグネチャは名前の後に続きます。シグネチャは帰納的宣言の適格要件に従って任意のパラメータを指定することができますが、シグネチャの戻り型は指定された帰納型の型コンストラクタを完全に適用したものでなければなりません。シグネチャが提供されない場合、コンストラクタの型は適格な戻り値を構成するのに十分な暗黙のパラメータを挿入することによって推測されます。 +コンストラクタの仕様は {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`where` の後に続きます。コンストラクタは必須ではありません。コンストラクタのない帰納型としては {lean}`False` と {lean}`Empty` などがまさに当てはまります。各コンストラクタの指定は、縦棒（`'|'`、Unicode `'VERTICAL BAR' (U+007c)`）・宣言修飾子・名前で始まります。名前は {tech}[生識別子] です。宣言シグネチャは名前の後に続きます。シグネチャは帰納的宣言の適格要件に従って任意のパラメータを指定することができますが、シグネチャの戻り型は指定された帰納型の型コンストラクタを完全に適用したものでなければなりません。シグネチャが提供されない場合、コンストラクタの型は適格な戻り値を構成するのに十分な暗黙のパラメータを挿入することによって推測されます。 :::comment The new inductive type's name is defined in the {tech}[current namespace]. @@ -131,13 +131,13 @@ Each constructor's name is in the inductive type's namespace.{index subterm:="of :::comment ## Parameters and Indices +::: + +## パラメータと添字 %%% tag := "inductive-datatypes-parameters-and-indices" %%% -::: - -## パラメータと添字 :::comment Type constructors may take two kinds of arguments: {deftech}_parameters_ {index subterm:="of inductive type"}[parameter] and {deftech key:="index"}_indices_.{index subterm:="of inductive type"}[index] @@ -461,13 +461,13 @@ inductive Either'' : Type u → Type v → Type (max u v) where :::comment ## Anonymous Constructor Syntax +::: + +## 匿名コンストラクタ構文 %%% tag := "anonymous-constructor-syntax" %%% -::: - -## 匿名コンストラクタ構文 :::comment If an inductive type has just one constructor, then this constructor is eligible for {deftech}_anonymous constructor syntax_. @@ -540,13 +540,13 @@ def AtLeastOne.head' : AtLeastOne α → α :::comment ## Deriving Instances +::: + +## インスタンスの導出 %%% tag := "inductive-declarations-deriving-instances" %%% -::: - -## インスタンスの導出 :::comment The optional {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`deriving` clause of an inductive type declaration can be used to derive instances of type classes. @@ -580,13 +580,13 @@ An inductive type's run-time representation depends both on how many constructor :::comment ## Exceptions +::: + +## 例外 %%% tag := "inductive-types-runtime-special-support" %%% -::: - -## 例外 :::comment Not every inductive type is represented as indicated here—some inductive types have special support from the Lean compiler: @@ -711,13 +711,13 @@ However, in cases where some representation is required (such as when they are a :::comment ## Trivial Wrappers +::: + +## 自明なラッパ %%% tag := "inductive-types-trivial-wrappers" %%% -::: - -## 自明なラッパ :::comment If an inductive type has exactly one constructor, and that constructor has exactly one run-time relevant parameter, then the inductive type is represented identically to its parameter. @@ -751,14 +751,14 @@ Thus, subtypes impose no runtime overhead in compiled code, and are represented :::comment ## Other Inductive Types +::: + +## その他の帰納型 %%% tag := "inductive-types-standard-representation" %%% -::: - -## その他の帰納型 :::comment If an inductive type doesn't fall into one of the categories above, then its representation is determined by its constructors. @@ -825,7 +825,7 @@ Within each group the fields are ordered in declaration order. **Warning**: Triv ::: * 最初の種類のフィールドにアクセスするには、 `lean_ctor_get(val, i)` を使って `i` 番目の非スカラーフィールドを取得します。 -* {lean}`USize` フィールドにアクセスするには、`lean_ctor_get_usize(val, n+i)` を使って `i` 番目の usize フィールドを取得します。`n` は最初の種類のフィールドの総数です。 +* {lean}`USize` フィールドにアクセスするには、`lean_ctor_get_usize(val, n+i)` を使って `i` 番目の `USize` フィールドを取得します。`n` は最初の種類のフィールドの総数です。 * その他のスカラーフィールドにアクセスするには、`lean_ctor_get_uintN(vai, off)` または `lean_ctor_get_usize(val, off)` を適切に使用します。ここで `off` は構造体内のフィールドのバイトオフセットであり、`n*sizeof(void*)` から始まります。`n` はその前の2種類のフィールドの数です。 ::::keepEnv @@ -882,14 +882,14 @@ Figure out how to test/validate/CI these statements :::comment # Mutual Inductive Types +::: + +# 相互帰納型 %%% tag := "mutual-inductive-types" %%% -::: - -# 相互帰納型 :::comment Inductive types may be mutually recursive. @@ -909,7 +909,7 @@ This distinction can also be expressed by the choice of one of two mutually indu ::: -先の例の型 {name}`EvenOddList` は真偽値の添字を使用して問題のリストの要素数が偶数か奇数かを選択しました。この区別は、2つの相互帰納的データ型 {name}`EvenList` と {name}`OddList` のどちらかを選択することでも表現できます： +先の例の型 {name}`EvenOddList` は真偽値の添字を使用して問題のリストの要素数が偶数か奇数かを選択しました。この区別は、2つの相互帰納型 {name}`EvenList` と {name}`OddList` のどちらかを選択することでも表現できます： ```lean mutual @@ -934,14 +934,14 @@ invalid dotted identifier notation, unknown identifier `OddList.nil` from expect :::comment ## Requirements +::: + +## 要件 %%% tag := "mutual-inductive-types-requirements" %%% -::: - -## 要件 :::comment The inductive types declared in a `mutual` block are considered as a group; they must collectively satisfy generalized versions of the well-formedness criteria for non-mutually-recursive inductive types. @@ -953,13 +953,13 @@ This is true even if they could be defined without the `mutual` block, because t :::comment ### Mutual Dependencies +::: + +### 相互依存 %%% tag := "mutual-inductive-types-dependencies" %%% -::: - -### 相互依存 :::comment Each type constructor's signature must be able to be elaborated without reference to the other inductive types in the `mutual` group. @@ -1005,13 +1005,13 @@ unknown identifier 'FreshList' :::comment ### Parameters Must Match +::: + +### マッチすべきパラメータ %%% tag := "mutual-inductive-types-same-parameters" %%% -::: - -### マッチすべきパラメータ :::comment All inductive types in the `mutual` group must have the same {tech}[parameters]. @@ -1080,13 +1080,13 @@ but is expected to have type :::comment ### Universe Levels +::: + +### 宇宙レベル %%% tag := "mutual-inductive-types-same-universe" %%% -::: - -### 宇宙レベル :::comment The universe levels of each inductive type in a mutual group must obey the same requirements as non-mutually-recursive inductive types. @@ -1204,7 +1204,7 @@ In other words, in the type of each parameter to each constructor in all the typ ::: -`mutual` グループで定義される各帰納型は、グループ内のすべての型のコンストラクタのパラメータの型中において strict positively にのみ出現可能です。言い換えると、グループ内のすべての型の各コンストラクタのパラメータの型では、グループ内のどの型コンストラクタも矢印の左側には出現せず、帰納的データ型の型コンストラクタの引き数でない限り引数の位置に出現しません。 +`mutual` グループで定義される各帰納型は、グループ内のすべての型のコンストラクタのパラメータの型中において strict positively にのみ出現可能です。言い換えると、グループ内のすべての型の各コンストラクタのパラメータの型では、グループ内のどの型コンストラクタも矢印の左側には出現せず、帰納型の型コンストラクタの引き数でない限り引数の位置に出現しません。 :::comment :: example "Mutual strict positivity" @@ -1261,13 +1261,13 @@ end :::comment ## Recursors +::: + +## 再帰子 %%% tag := "mutual-inductive-types-recursors" %%% -::: - -## 再帰子 :::comment Mutual inductive types are provided with primitive recursors, just like non-mutually-defined inductive types. @@ -1355,13 +1355,13 @@ Two.rec.{u} {α : Type} :::comment ## Run-Time Representation +::: + +## ランタイム表現 %%% tag := "mutual-inductive-types-run-time" %%% -::: - -## ランタイム表現 :::comment Mutual inductive types are represented identically to {ref "run-time-inductives"}[non-mutual inductive types] in compiled code and in the runtime. diff --git a/Manual/Language/InductiveTypes/LogicalModel.lean b/Manual/Language/InductiveTypes/LogicalModel.lean index 07c1a59..e9d436a 100644 --- a/Manual/Language/InductiveTypes/LogicalModel.lean +++ b/Manual/Language/InductiveTypes/LogicalModel.lean @@ -24,13 +24,13 @@ tag := "inductive-types-logical-model" :::comment # Recursors +::: + +# 再帰子（Recursors） %%% tag := "recursors" %%% -::: - -# 再帰子（Recursors） :::comment Every inductive type is equipped with a {tech}[recursors]. @@ -43,14 +43,14 @@ Recursors have function types, but they are primitive and are not definable usin :::comment ## Recursor Types +::: + +## 再帰子の型（Recursor Types） %%% tag := "recursor-types" %%% -::: - -## 再帰子の型（Recursor Types） :::comment The recursor takes the following parameters: @@ -127,7 +127,7 @@ The result type of the recursor is the motive applied to these indices and the t ::: - * 動機は Bool から任意の宇宙における型を計算します。 + * 動機は {lean}`Bool` から任意の宇宙における型を計算します。 * {lean}`false` と {lean}`true` の両方で動機が満たされる両方のコンストラクタのケースが存在します。 * ターゲットはなんらかの {lean}`Bool` です。 @@ -402,13 +402,13 @@ This means that proofs of equality can be used to rewrite the types of non-propo :::comment ## Reduction +::: + +## 簡約（Reduction） %%% tag := "iota-reduction" %%% -::: - -## 簡約（Reduction） :::comment In addition to adding new constants to the logic, inductive type declarations also add new reduction rules. @@ -607,7 +607,7 @@ Because they are largely useless, Lean's inductive type elaborator has not been ::: -Lean は実用上多相的に使うことができない宇宙多相型を拒否します。これは宇宙パラメータの特定のインスタンス化によって型自体が {lean}`Prop` になる場合に発生する可能性があります。この型が {tech}[subsingleton] でない場合、再帰子は命題のみを対象とすることができます（つまり、 {tech}[動機] は {lean}`Prop` を返さなければなりません）。このような型は {lean}`Prop` そのものとしてしか意味をなさないため、宇宙多相としたことは間違いだと考えられます。これらの型はほとんど役に立たないため、Lean のデータ型エラボレータはこれらの型をサポートするように設計されていません。 +Lean は実用上多相的に使うことができない宇宙多相型を拒否します。これは宇宙パラメータの特定のインスタンス化によって型自体が {lean}`Prop` になる場合に発生する可能性があります。この型が {tech}[subsingleton] でない場合、再帰子は命題のみを対象とすることができます（つまり、 {tech}[動機] は {lean}`Prop` を返さなければなりません）。このような型は {lean}`Prop` そのものとしてしか意味をなさないため、宇宙多相としたことは間違いだと考えられます。これらの型はほとんど役に立たないため、Lean の帰納型エラボレータはこれらの型をサポートするように設計されていません。 :::comment When such universe-polymorphic inductive types are indeed subsingletons, it can make sense to define them. diff --git a/Manual/Language/InductiveTypes/Structures.lean b/Manual/Language/InductiveTypes/Structures.lean index 03a09d3..a5fa5da 100644 --- a/Manual/Language/InductiveTypes/Structures.lean +++ b/Manual/Language/InductiveTypes/Structures.lean @@ -46,7 +46,7 @@ Structures do not add any expressive power to Lean; all of their features are im ::: -{deftech}[構造体] （structure）は単一のコンストラクタと添字を持たない帰納型です。これらの制限と引き換えに、Lean は構造体のための数々の便利なコードを生成します：アクセサ関数が各フィールドに対して生成される・位置引数ではなくフィールド名に基づく追加のコンストラクタ構文が利用できる・同様の構文を使用して特定の名前付きフィールドの値を書き換えることができる・構造体は他の構造体を拡張することができる。構造体は Lean の表現力を増すものではありません；すべての機能はコード生成の観点から実装されます。 +{deftech}[構造体] （structure）は単一のコンストラクタと添字を持たない帰納型です。これらの制限と引き換えに、Lean は構造体のための数々の便利なコードを生成します：アクセサ関数が各フィールドに対して生成される・位置引数ではなくフィールド名に基づく追加のコンストラクタ構文が利用できる・同様の構文を使用して特定の名前付きフィールドの値を書き換えることができる・構造体は他の構造体を拡張することができる。他の帰納型と同様に、構造体も再帰的です；また strict positivity に関しても同じ制約を受けます。構造体は Lean の表現力を増すものではありません；すべての機能はコード生成の観点から実装されます。 ```lean (show := false) -- Test claim about recursive above @@ -62,13 +62,13 @@ structure RecStruct where :::comment # Structure Parameters +::: + +# 構造体のパラメータ（Structure Parameters） %%% tag := "structure-params" %%% -::: - -# 構造体のパラメータ（Structure Parameters） :::comment Just like ordinary inductive type declarations, the header of the structure declaration contains a signature that may specify both parameters and a resulting universe. @@ -80,13 +80,13 @@ Structures may not define {tech}[indexed families]. :::comment # Fields +::: + +# フィールド（Fields） %%% tag := "structure-fields" %%% -::: - -# フィールド（Fields） :::comment Each field of a structure declaration corresponds to a parameter of the constructor. @@ -223,14 +223,14 @@ Fields are numbered beginning with `1`. :::comment # Structure Constructors +::: + +# 構造体のコンストラクタ（Structure Constructors） %%% tag := "structure-constructors" %%% -::: - -# 構造体のコンストラクタ（Structure Constructors） :::comment Structure constructors may be explicitly named by providing the constructor name and `::` prior to the fields. diff --git a/Manual/NotationsMacros.lean b/Manual/NotationsMacros.lean index ad607e3..e0af677 100644 --- a/Manual/NotationsMacros.lean +++ b/Manual/NotationsMacros.lean @@ -59,7 +59,7 @@ They can be combined flexibly to achieve the necessary results: tag := "macros" %%% -{deftech}_Macros_ are transformations from {name Lean.Syntax}`Syntax` to {name Lean.Syntax}`Syntax` that occur during {tech key:="elaborator"}[elaboration] and during {ref "tactic-macros"}[tactic execution]. +{deftech}_Macros_ are transformations from {name Lean.Syntax}`Syntax` to {name Lean.Syntax}`Syntax` that occur during {tech key:="エラボレータ"}[elaboration] and during {ref "tactic-macros"}[tactic execution]. Replacing syntax with the result of transforming it with a macro is called {deftech}_macro expansion_. Multiple macros may be associated with a single {tech}[syntax kind], and they are attempted in order of definition. Macros are run in a {tech}[monad] that has access to some compile-time metadata and has the ability to either emit an error message or to delegate to subsequent macros, but the macro monad is much less powerful than the elaboration monads. @@ -184,7 +184,7 @@ tag := "macro-monad" The macro monad {name Lean.MacroM}`MacroM` is sufficiently powerful to implement hygiene and report errors. Macro expansion does not have the ability to modify the environment directly, to carry out unification, to examine the current local context, or to do anything else that only makes sense in one particular context. -This allows the same macro mechanism to be used throughout Lean, and it makes macros much easier to write than {tech}[elaborators]. +This allows the same macro mechanism to be used throughout Lean, and it makes macros much easier to write than {tech}[エラボレータ]elaborators. {docstring Lean.MacroM} diff --git a/Manual/NotationsMacros/Notations.lean b/Manual/NotationsMacros/Notations.lean index 4c9a616..4ae1dff 100644 --- a/Manual/NotationsMacros/Notations.lean +++ b/Manual/NotationsMacros/Notations.lean @@ -63,7 +63,7 @@ If this still does not resolve the ambiguity, then all are saved, and the elabor Rather than a single operator with its fixity and token, the body of a notation declaration consists of a sequence of {deftech}_notation items_, which may be either new {tech}[atoms] (including both keywords such as `if`, `#eval`, or `where` and symbols such as `=>`, `+`, `↗`, `⟦`, or `⋉`) or positions for terms. Just as they do in operators, string literals identify the placement of atoms. -Leading and trailing spaces in the strings do not affect parsing, but they cause Lean to insert spaces in the corresponding position when displaying the syntax in {tech}[proof states] and error messages. +Leading and trailing spaces in the strings do not affect parsing, but they cause Lean to insert spaces in the corresponding position when displaying the syntax in {tech}[証明状態]proof states and error messages. Identifiers indicate positions where terms are expected, and name the corresponding term so it can be inserted in the notation's expansion. While custom operators have a single notion of precedence, there are many involved in a notation. @@ -183,7 +183,7 @@ def e : Nat × Int := When the expansion consists of the application of a function defined in the global environment and each term in the notation occurs exactly once, an {tech}[unexpander] is generated. -The new notation will be displayed in {tech}[proof states], error messages, and other output from Lean when matching function application terms otherwise would have been displayed. +The new notation will be displayed in {tech}[証明状態]proof states, error messages, and other output from Lean when matching function application terms otherwise would have been displayed. As with custom operators, Lean does not track whether the notation was used in the original term; it is used at every opportunity in Lean's output. # Operators and Notations diff --git a/Manual/NotationsMacros/Operators.lean b/Manual/NotationsMacros/Operators.lean index 0e2d5bc..18f87dd 100644 --- a/Manual/NotationsMacros/Operators.lean +++ b/Manual/NotationsMacros/Operators.lean @@ -307,7 +307,7 @@ prefix:max "blah" => Nat.add ``` If the term consists either of a name from the global environment or of an application of such a name to one or more arguments, then Lean automatically generates an {tech}[unexpander] for the operator. -This means that the operator will be displayed in {tech}[proof states], error messages, and other output from Lean when the function term otherwise would have been displayed. +This means that the operator will be displayed in {tech}[証明状態]proof states, error messages, and other output from Lean when the function term otherwise would have been displayed. Lean does not track whether the operator was used in the original term; it is inserted at every opportunity. :::::keepEnv diff --git a/Manual/NotationsMacros/SyntaxDef.lean b/Manual/NotationsMacros/SyntaxDef.lean index dda147c..c4eb141 100644 --- a/Manual/NotationsMacros/SyntaxDef.lean +++ b/Manual/NotationsMacros/SyntaxDef.lean @@ -512,7 +512,7 @@ String literals are parsed as {tech}[atoms] (including both keywords such as `if ```grammar $s:str ``` -Leading and trailing spaces in the strings do not affect parsing, but they cause Lean to insert spaces in the corresponding position when displaying the syntax in {tech}[proof states] and error messages. +Leading and trailing spaces in the strings do not affect parsing, but they cause Lean to insert spaces in the corresponding position when displaying the syntax in {tech}[証明状態]proof states and error messages. Ordinarily, valid identifiers occurring as atoms in syntax rules become reserved keywords. Preceding a string literal with an ampersand (`&`) suppresses this behavior: ```grammar diff --git a/Manual/Simp.lean b/Manual/Simp.lean index 437ab93..ca84a2b 100644 --- a/Manual/Simp.lean +++ b/Manual/Simp.lean @@ -35,14 +35,14 @@ The simplifier is highly configurable, and a number of tactics use it in differe :::comment # Invoking the Simplifier +::: + +# 単純化器の呼び出し（Invoking the Simplifier） %%% tag := "simp-tactic-naming" %%% -::: - -# 単純化器の呼び出し（Invoking the Simplifier） :::comment Lean's simplifier can be invoked in a variety of ways. @@ -163,7 +163,7 @@ In other words, an invocation of a simplification tactic takes the following mod ::: 言い換えれば、単純化タクティクの呼び出しは以下の修飾子を順番に取ります。またこれらはすべて任意です： - * 呼び出される単純化器が {tactic}`simp` のバージョンか {tactic}`dsimp` のバージョンであるかに応じて、 {name}`Lean.Meta.Simp.Config` か {name}`Lean.Meta.DSimp.Config` のインスタンスでなければなりません。 + * {ref "tactic-config"}[設定オプション] 、呼び出される単純化器が {tactic}`simp` のバージョンか {tactic}`dsimp` のバージョンであるかに応じて、 {name}`Lean.Meta.Simp.Config` か {name}`Lean.Meta.DSimp.Config` のフィールドでなければなりません。 * {keywordOf Lean.Parser.Tactic.simp}`only` 修飾子はデフォルトの simp セットを除外し、代わりに空の {margin}[厳密には、再帰的なケースを除外するために、simp セットは常に {name}`eq_self` と {name}`iff_self` を含みます。] simp セットから開始します。 * 補題リストは simp セットに補題を追加したり削除したりします。補題リストで補題を指定する方法は3つあります： * `*`、これは証明状態にあるすべての仮定を simp セットに追加します @@ -323,13 +323,13 @@ h' : p (x + 12) :::comment # Rewrite Rules +::: + +# 書き換え規則（Rewrite Rules） %%% tag := "simp-rewrites" %%% -::: - -# 書き換え規則（Rewrite Rules） :::comment The simplifier has three kinds of rewrite rules: @@ -347,7 +347,7 @@ The simplifier has three kinds of rewrite rules: : 定義の展開 - 単純化器はデフォルトで {tech}[reducible] な定義のみを展開します。しかし、任意の {tech}[semireducible] または {tech}[irreducible] な定義用に書き換え規則を追加して、単純化器が同様にそれらを展開するようにできます。単純化器が定義上モード（ {tactic}`dsimp` とその亜種）で動作している場合、定義の展開は定義された名前をその値で置き換えるだけです；それ以外では、等式のコンパイラから提供された等式の補題も使用します。 + 単純化器はデフォルトで {tech}[reducible] な定義のみを展開します。しかし、任意の {tech}[semi-reducible] または {tech}[irreducible] な定義用に書き換え規則を追加して、単純化器が同様にそれらを展開するようにできます。単純化器が定義上モード（ {tactic}`dsimp` とその亜種）で動作している場合、定義の展開は定義された名前をその値で置き換えるだけです；それ以外では、等式のコンパイラから提供された等式の補題も使用します。 :::comment : Equational lemmas @@ -511,13 +511,13 @@ Even when the simp set is empty, {tactic}`simp` can replace `let`-bound variable :::comment # Simp sets +::: + +# simp セット（Simp sets） %%% tag := "simp-sets" %%% -::: - -# simp セット（Simp sets） :::comment A collection of rules used by the simplifier is called a {deftech}_simp set_. @@ -583,14 +583,14 @@ The {tactic}`simp` tactics can be instructed to use the new simp set by includin :::comment # Simp Normal Forms +::: + +# simp 正規形（Simp Normal Forms） %%% tag := "simp-normal-forms" %%% -::: - -# simp 正規形（Simp Normal Forms） :::comment The default {tech}[simp set] contains all the theorems and simplification procedures marked with the {attr}`simp` attribute. @@ -640,13 +640,13 @@ If a library relies on additional simplification rules for definitions or declar :::comment # Terminal vs Non-Terminal Positions +::: + +# 終端・非終端位置（Terminal vs Non-Terminal Positions） %%% tag := "terminal-simp" %%% -::: - -# 終端・非終端位置（Terminal vs Non-Terminal Positions） :::comment To write maintainable proofs, avoid using {tactic}`simp` without {keywordOf Lean.Parser.Tactic.simp}`only` unless it closes the goal. @@ -736,13 +736,13 @@ tag := "simp-config" :::comment ## Options +::: + +## オプション（Options） %%% tag := "simp-options" %%% -::: - -## オプション（Options） :::comment Some global options affect {tactic}`simp`: @@ -763,14 +763,14 @@ Some global options affect {tactic}`simp`: :::comment # Simplification vs Rewriting +::: + +# 単純化と書き換え（Simplification vs Rewriting） %%% tag := "simp-vs-rw" %%% -::: - -# 単純化と書き換え（Simplification vs Rewriting） :::comment Both {tactic}`simp` and {tactic}`rw`/{tactic}`rewrite` use equational lemmas to replace parts of terms with equivalent alternatives. diff --git a/Manual/Tactics.lean b/Manual/Tactics.lean index bacaabf..d89e47a 100644 --- a/Manual/Tactics.lean +++ b/Manual/Tactics.lean @@ -109,13 +109,13 @@ Tactic proofs may be embedded via {keywordOf Lean.Parser.Term.byTactic}`by` in a :::comment # Reading Proof States +::: + +# 証明状態の読み方（Reading Proof States） %%% tag := "proof-states" %%% -::: - -# 証明状態の読み方（Reading Proof States） :::comment The goals in a proof state are displayed in order, with the main goal on top. @@ -476,13 +476,13 @@ This is generally not a good idea for non-propositions, however—when it matter :::comment ## Hiding Proofs and Large Terms +::: + +## 証明と大きな項の非表示（Hiding Proofs and Large Terms） %%% tag := "hiding-terms-in-proof-states" %%% -::: - -## 証明と大きな項の非表示（Hiding Proofs and Large Terms） :::comment Terms in proof states can be quite big, and there may be many assumptions. @@ -544,13 +544,13 @@ Printing very large terms can lead to slowdowns or even stack overflows in tooli :::comment ## Metavariables +::: + +## メタ変数（Metavariables） %%% tag := "metavariables-in-proofs" %%% -::: - -## メタ変数（Metavariables） :::comment Terms that begin with a question mark are _metavariables_ that correspond to an unknown value. @@ -737,13 +737,13 @@ Demonstrate and explain diff labels that show the difference between the steps o :::comment # The Tactic Language +::: + +# タクティク言語（The Tactic Language） %%% tag := "tactic-language" %%% -::: - -# タクティク言語（The Tactic Language） :::comment A tactic script consists of a sequence of tactics, separated either by semicolons or newlines. @@ -775,13 +775,13 @@ However, with a few exceptions, the majority of tactics can be identified by a l :::comment ## Control Structures +::: + +## 制御構造（Control Structures） %%% tag := "tactic-language-control" %%% -::: - -## 制御構造（Control Structures） :::comment Strictly speaking, there is no fundamental distinction between control structures and other tactics. @@ -795,13 +795,13 @@ The tactics in this section are those that resemble traditional control structur :::comment ### Success and Failure +::: + +### 成功と失敗（Success and Failure） %%% tag := "tactic-language-success-failure" %%% -::: - -### 成功と失敗（Success and Failure） :::comment When run in a proof state, every tactic either succeeds or fails. @@ -827,13 +827,13 @@ Unlike exceptions, there is no operator to distinguish between reasons for failu :::comment ### Branching +::: + +### 分岐（Branching） %%% tag := "tactic-language-branching" %%% -::: - -### 分岐（Branching） :::comment Tactic proofs may use pattern matching and conditionals. @@ -908,14 +908,14 @@ example (n : Nat) : if n = 0 then n < 1 else n > 0 := by :::comment ### Goal Selection +::: + +### ゴールの選択（Goal Selection） %%% tag := "tactic-language-goal-selection" %%% -::: - -### ゴールの選択（Goal Selection） :::comment Most tactics affect the {tech}[main goal]. @@ -941,13 +941,13 @@ Goal selection tactics provide a way to treat a different goal as the main one, :::comment #### Sequencing +::: + +#### 順序実行（Sequencing） %%% tag := "tactic-language-sequencing" %%% -::: - -#### 順序実行（Sequencing） :::comment In addition to running tactics one after the other, each being used to solve the main goal, the tactic language supports sequencing tactics according to the way in which goals are produced. @@ -1070,13 +1070,13 @@ Replacing the `;` with {tactic}`<;>` and running {tacticStep}`cases h <;> simp [ :::comment #### Working on Multiple Goals +::: + +#### 複数のゴールに作用する（Working on Multiple Goals） %%% tag := "tactic-language-multiple-goals" %%% -::: - -#### 複数のゴールに作用する（Working on Multiple Goals） :::comment The tactics {tactic}`all_goals` and {tactic}`any_goals` allow a tactic to be applied to every goal in the proof state. @@ -1095,13 +1095,13 @@ The difference between them is that if the tactic fails for in any of the goals, :::comment ### Focusing +::: + +### 焦点をあてる（Focusing） %%% tag := "tactic-language-focusing" %%% -::: - -### 焦点をあてる（Focusing） :::comment Focusing tactics remove some subset of the proof goals (typically leaving only the main goal) from the consideration of some further tactics. @@ -1131,13 +1131,13 @@ This makes it easier to read and maintain proofs, because the connections betwee :::comment ### Repetition and Iteration +::: + +### 繰り返しと反復（Repetition and Iteration） %%% tag := "tactic-language-iteration" %%% -::: - -### 繰り返しと反復（Repetition and Iteration） :::tactic "iterate" ::: @@ -1154,13 +1154,13 @@ tag := "tactic-language-iteration" :::comment ## Names and Hygiene +::: + +## 名前と健全性（Names and Hygiene） %%% tag := "tactic-language-hygiene" %%% -::: - -## 名前と健全性（Names and Hygiene） :::comment Behind the scenes, tactics generate proof terms. @@ -1271,13 +1271,13 @@ n : Nat :::comment ### Accessing Assumptions +::: + +### 仮定へのアクセス（Accessing Assumptions） %%% tag := "tactic-language-assumptions" %%% -::: - -### 仮定へのアクセス（Accessing Assumptions） :::comment Many tactics provide a means of specifying names for the assumptions that they introduce. @@ -1293,13 +1293,13 @@ When an assumption does not have a name, one can be assigned using {tactic}`next :::comment ## Assumption Management +::: + +## 仮定の管理（Assumption Management） %%% tag := "tactic-language-assumption-management" %%% -::: - -## 仮定の管理（Assumption Management） :::comment Larger proofs can benefit from management of proof states, removing irrelevant assumptions and making their names easier to understand. @@ -1321,13 +1321,13 @@ Along with these operators, {tactic}`rename_i` allows inaccessible assumptions t :::comment ## Local Definitions and Proofs +::: + +## ローカル定義と証明（Local Definitions and Proofs） %%% tag := "tactic-language-local-defs" %%% -::: - -## ローカル定義と証明（Local Definitions and Proofs） :::comment {tactic}`have` and {tactic}`let` both create local assumptions. @@ -1358,25 +1358,43 @@ Generally speaking, {tactic}`have` should be used when proving an intermediate l :::tactic Lean.Parser.Tactic.tacticLet'_ ::: +:::comment ## Configuration +::: +## 設定（Configuration） %%% tag := "tactic-config" %%% +:::comment Many tactics are configurable.{index subterm:="of tactics"}[configuration] By convention, tactics share a configuration syntax, described using {syntaxKind}`optConfig`. The specific options available to each tactic are described in the tactic's documentation. -:::syntax Lean.Parser.Tactic.optConfig (open := false) +::: + +多くのタクティクは設定変更が可能です。 {index subterm:="of tactics"}[configuration] 慣例的に、タクティクは設定の構文を共有しており、 {syntaxKind}`optConfig` を使って記述します。各タクティクで利用可能なオプションはタクティクのドキュメントに記述されています。 + +::::syntax Lean.Parser.Tactic.optConfig (open := false) +:::comment A tactic configuration consists of zero or more {deftech}[configuration items]: +::: + +タクティクの設定は0個以上の {deftech}[設定項目] （configuration item）から構成されます： + ```grammar $x:configItem* ``` -::: +:::: -:::syntax Lean.Parser.Tactic.configItem (open := false) +::::syntax Lean.Parser.Tactic.configItem (open := false) +:::comment Each configuration item has a name that corresponds to an underlying tactic option. Boolean options may be enabled or disabled using prefix `+` and `-`: +::: + +各設定項目は、タクティクのオプションに対応する名前を持ちます。真偽値のオプションは、接頭辞 `+` と `-` を使って有効・無効に設定できます： + ```grammar +$x ``` @@ -1384,28 +1402,38 @@ Boolean options may be enabled or disabled using prefix `+` and `-`: -$x ``` +:::comment Options may be assigned specific values using a syntax similar to that for named function arguments: +::: + +オプションは、名前付き関数の引数の構文に似た構文を使って特定の値を割り当てることができます： + ```grammar ($x:ident := $t) ``` +:::comment Finally, the name `config` is reserved; it is used to pass an entire set of options as a data structure. The specific type expected depends on the tactic. +::: + +最後に、`config` という名前が予約されています；これはオプションのセット全体をデータ構造として渡すために使われます。期待される具体的な型はタクティクによって異なります。 + ```grammar (config := $t) ``` -::: +:::: :::comment ## Namespace and Option Management +::: + +## 名前空間とオプション管理（Namespace and Option Management） %%% tag := "tactic-language-namespaces-options" %%% -::: - -## 名前空間とオプション管理（Namespace and Option Management） :::comment Namespaces and options can be adjusted in tactic scripts using the same syntax as in terms. @@ -1422,13 +1450,13 @@ Namespaces and options can be adjusted in tactic scripts using the same syntax a :::comment ### Controlling Unfolding +::: + +### 展開のコントロール（Controlling Unfolding） %%% tag := "tactic-language-unfolding" %%% -::: - -### 展開のコントロール（Controlling Unfolding） :::comment By default, only definitions marked reducible are unfolded, except when checking definitional equality. @@ -1450,13 +1478,13 @@ These operators allow this default to be adjusted for some part of a tactic scri :::comment # Options +::: + +# オプション %%% tag := "tactic-language-options" %%% -::: - -# オプション :::comment These options affect the meaning of tactics. diff --git a/Manual/Tactics/Conv.lean b/Manual/Tactics/Conv.lean index 81e526f..2c59d50 100644 --- a/Manual/Tactics/Conv.lean +++ b/Manual/Tactics/Conv.lean @@ -103,14 +103,14 @@ example : (fun (x y z : Nat) => x + (y + z)) = (fun x y z => (z + x) + y) := by :::comment # Control Structures +::: + +# 制御構造（Control Structures） %%% tag := "conv-control" %%% -::: - -# 制御構造（Control Structures） :::conv first show := "first" ::: @@ -138,14 +138,14 @@ tag := "conv-control" :::comment # Goal Selection +::: + +# ゴールの選択（Goal Selection） %%% tag := "conv-goals" %%% -::: - -# ゴールの選択（Goal Selection） :::conv allGoals show:= "all_goals" ::: @@ -177,14 +177,14 @@ tag := "conv-goals" :::comment # Navigation +::: + +# 移動（Navigation） %%% tag := "conv-nav" %%% -::: - -# 移動（Navigation） :::conv lhs show:= "lhs" ::: @@ -247,14 +247,14 @@ tag := "conv-change" :::comment ## Reduction +::: + +## 簡約（Reduction） %%% tag := "conv-reduction" %%% -::: - -## 簡約（Reduction） :::conv whnf show:= "whnf" ::: @@ -291,13 +291,13 @@ tag := "conv-simp" :::comment ## Rewriting +::: + +## 書き換え（Rewriting） %%% tag := "conv-rw" %%% -::: - -## 書き換え（Rewriting） :::conv change show:= "change" ::: @@ -316,14 +316,14 @@ tag := "conv-rw" :::comment # Nested Tactics +::: + +# 入れ子のタクティク（Nested Tactics） %%% tag := "conv-nested" %%% -::: - -# 入れ子のタクティク（Nested Tactics） :::tactic Lean.Parser.Tactic.Conv.convTactic ::: @@ -343,13 +343,13 @@ tag := "conv-nested" :::comment # Debugging Utilities +::: + +# デバッグ用ユーティリティ（Debugging Utilities） %%% tag := "conv-debug" %%% -::: - -# デバッグ用ユーティリティ（Debugging Utilities） :::conv convTrace_state show:= "trace_state" ::: @@ -357,13 +357,13 @@ tag := "conv-debug" :::comment # Other +::: + +# その他（Other） %%% tag := "conv-other" %%% -::: - -# その他（Other） :::conv convRfl show:= "rfl" ::: diff --git a/Manual/Tactics/Custom.lean b/Manual/Tactics/Custom.lean index e95ee30..91cc6c9 100644 --- a/Manual/Tactics/Custom.lean +++ b/Manual/Tactics/Custom.lean @@ -49,13 +49,13 @@ A custom tactic consists of an extension to the `tactic` category along with eit :::comment # Tactic Macros +::: + +# タクティクマクロ（Tactic Macros） %%% tag := "tactic-macros" %%% -::: - -# タクティクマクロ（Tactic Macros） :::comment The easiest way to define a new tactic is as a {tech}[macro] that expands into already-existing tactics. @@ -113,14 +113,14 @@ Otherwise, the syntax will be interpreted as that of a term, which will match ag :::comment ## Extensible Tactic Macros +::: + +## 拡張可能なタクティクマクロ（Extensible Tactic Macros） %%% tag := "tactic-macro-extension" %%% -::: - -## 拡張可能なタクティクマクロ（Extensible Tactic Macros） :::comment Because macro expansion can fail, {TODO}[xref] multiple macros can match the same syntax, allowing backtracking. @@ -208,13 +208,13 @@ Backtracking is at the granularity of {keywordOf Lean.Parser.Command.macro_rules :::comment # The Tactic Monad +::: + +# タクティクモナド（The Tactic Monad） %%% tag := "tactic-monad" %%% -::: - -# タクティクモナド（The Tactic Monad） ::: planned 67 * Relationship to {name}`Lean.Elab.Term.TermElabM`, {name}`Lean.Meta.MetaM` diff --git a/Manual/Tactics/Reference.lean b/Manual/Tactics/Reference.lean index 874150e..454f3ea 100644 --- a/Manual/Tactics/Reference.lean +++ b/Manual/Tactics/Reference.lean @@ -32,13 +32,13 @@ tag := "tactic-ref" :::comment # Assumptions +::: + +# 仮定（Assumptions） %%% tag := "tactic-ref-assumptions" %%% -::: - -# 仮定（Assumptions） :::tactic Lean.Parser.Tactic.assumption ::: @@ -48,13 +48,13 @@ tag := "tactic-ref-assumptions" :::comment # Quantifiers +::: + +# 量化子（Quantifiers） %%% tag := "tactic-ref-quantifiers" %%% -::: - -# 量化子（Quantifiers） :::tactic "exists" ::: @@ -75,13 +75,13 @@ tag := "tactic-ref-quantifiers" :::comment # Relations +::: + +# 関係（Relations） %%% tag := "tactic-ref-relations" %%% -::: - -# 関係（Relations） :::planned 47 * Descriptions of the `symm` and `refl` and `trans` attributes @@ -110,13 +110,13 @@ tag := "tactic-ref-relations" :::comment ## Equality +::: + +## 等価性（Equality） %%% tag := "tactic-ref-equality" %%% -::: - -## 等価性（Equality） :::tactic "subst" ::: @@ -138,13 +138,13 @@ tag := "tactic-ref-equality" :::comment # Lemmas +::: + +# 補題（Lemmas） %%% tag := "tactic-ref-lemmas" %%% -::: - -# 補題（Lemmas） :::tactic "exact" ::: @@ -167,13 +167,13 @@ tag := "tactic-ref-lemmas" :::comment # Falsehood +::: + +# 偽（Falsehood） %%% tag := "tactic-ref-false" %%% -::: - -# 偽（Falsehood） :::tactic "exfalso" ::: @@ -187,13 +187,13 @@ tag := "tactic-ref-false" :::comment # Goal Management +::: + +# ゴールの管理（Goal Management） %%% tag := "tactic-ref-goals" %%% -::: - -# ゴールの管理（Goal Management） :::tactic "suffices" ::: @@ -222,13 +222,13 @@ tag := "tactic-ref-goals" :::comment # Cast Management +::: + +# キャストの管理（Cast Management） %%% tag := "tactic-ref-casts" %%% -::: - -# キャストの管理（Cast Management） :::comment The tactics in this section make it easier avoid getting stuck on {deftech}_casts_, which are functions that coerce data from one type to another, such as converting a natural number to the corresponding integer. @@ -236,7 +236,7 @@ They are described in more detail by {citet castPaper}[]. ::: -本節のタクティクは {deftech}_キャスト_ （cast）に詰まってしまうことを回避します。キャストとはある型から別の型にデータを強制する関数であり、例えば自然数を対応する整数に変換するようなものです。これらは Robert Y. Lewis と Paul-Nicolas Madelaine による [_Simplifying Casts and Coercions_](https://arxiv.org/abs/2001.10594) で詳しく説明されています。 +本節のタクティクは {deftech}_キャスト_ （cast）に詰まってしまうことを回避します。キャストとはある型から別の型にデータを強制する関数であり、例えば自然数を対応する整数に変換するようなものです。これらは {citet castPaper}[] にて詳しく説明されています。 :::tactic Lean.Parser.Tactic.tacticNorm_cast_ ::: @@ -258,13 +258,13 @@ They are described in more detail by {citet castPaper}[]. :::comment # Extensionality +::: + +# 外延性（Extensionality） %%% tag := "tactic-ref-ext" %%% -::: - -# 外延性（Extensionality） :::tactic "ext" ::: @@ -282,13 +282,13 @@ tag := "tactic-ref-ext" # 書き換え（Rewriting） - -:::comment -# Rewriting %%% tag := "tactic-ref-rw" %%% + +:::comment +# Rewriting ::: :::tactic "rw" ::: @@ -325,23 +325,23 @@ Implemented by {name}`Lean.Elab.Tactic.evalUnfold`. :::comment # Inductive Types +::: + +# 帰納型（Inductive Types） %%% tag := "tactic-ref-inductive" %%% -::: - -# 帰納型（Inductive Types） :::comment ## Introduction +::: + +## 帰納法（Introduction） %%% tag := "tactic-ref-inductive-intro" %%% -::: - -## 帰納法（Introduction） :::tactic "constructor" ::: @@ -361,13 +361,13 @@ tag := "tactic-ref-inductive-intro" :::comment ## Elimination +::: + +## 除去（Elimination） %%% tag := "tactic-ref-inductive-elim" %%% -::: - -## 除去（Elimination） :::planned 48 @@ -394,13 +394,13 @@ Description of the `@[induction_eliminator]` and `@[cases_eliminator]` attribute :::comment # Library Search +::: + +# ライブラリ検索（Library Search） %%% tag := "tactic-ref-search" %%% -::: - -# ライブラリ検索（Library Search） :::comment The library search tactics are intended for interactive use. @@ -460,14 +460,14 @@ Try this: exact Nat.lt_trans h1 h2 :::comment # Case Analysis +::: + +# ケース分析（Case Analysis） %%% tag := "tactic-ref-cases" %%% -::: - -# ケース分析（Case Analysis） :::tactic "split" ::: @@ -477,14 +477,14 @@ tag := "tactic-ref-cases" :::comment # Decision Procedures +::: + +# 決定手続き（Decision Procedures） %%% tag := "tactic-ref-decision" %%% -::: - -# 決定手続き（Decision Procedures） :::tactic Lean.Parser.Tactic.decide show:="decide" ::: @@ -501,13 +501,13 @@ tag := "tactic-ref-decision" :::comment ## SAT Solver Integration +::: + +## SAT ソルバの統合（SAT Solver Integration） %%% tag := "tactic-ref-sat" %%% -::: - -## SAT ソルバの統合（SAT Solver Integration） :::tactic "bv_decide" ::: @@ -523,14 +523,14 @@ tag := "tactic-ref-sat" :::comment # Control Flow +::: + +# フロー制御（Control Flow） %%% tag := "tactic-ref-control" %%% -::: - -# フロー制御（Control Flow） :::tactic "skip" ::: @@ -564,14 +564,14 @@ tag := "tactic-ref-control" :::comment # Term Elaboration Backends +::: + +# 項エラボレーションのバックエンド（Term Elaboration Backends） %%% tag := "tactic-ref-term-helpers" %%% -::: - -# 項エラボレーションのバックエンド（Term Elaboration Backends） :::comment These tactics are used during elaboration of terms to satisfy obligations that arise. @@ -602,14 +602,14 @@ These tactics are used during elaboration of terms to satisfy obligations that a :::comment # Debugging Utilities +::: + +# デバッグ用ユーティリティ（Debugging Utilities） %%% tag := "tactic-ref-debug" %%% -::: - -# デバッグ用ユーティリティ（Debugging Utilities） :::tactic "sorry" ::: @@ -629,13 +629,13 @@ tag := "tactic-ref-debug" :::comment # Other +::: + +# その他（Other） %%% tag := "tactic-ref-other" %%% -::: - -# その他（Other） :::tactic "trivial" :::