Reference/Conv翻訳 (#12)

* 翻訳開始

* 翻訳完了

GLOSSARY.md

@@ -43,6 +43,7 @@
 | constructor | コンストラクタ | |
 | content | 内容 | |
 | context | （プログラム中のcontextの意で）コンテキスト、（文章中のcontextの意で）文脈 | |
+| conversion | 変換 | |
 | core language | コア言語 | |
 | core type theory | コア型理論 | |
 | curly brace | 波括弧 | |
@@ -253,6 +254,7 @@
 | trivial | 自明な | |
 | trust | 信頼 | |
 | tuple | タプル | |
+| turnstile | ターンスタイル | |
 | type class | 型クラス | |
 | type class instance synthesis | 型クラスインスタンス合成 | |
 | type signature | 型シグネチャ | |

Manual/Tactics/Conv.lean

@@ -17,25 +17,46 @@ set_option pp.rawOnError true
 
 set_option linter.unusedVariables false
 
+/-
 #doc (Manual) "Targeted Rewriting with {tactic}`conv`" =>
+-/
+#doc (Manual) "{tactic}`conv` によるターゲットの書き換え（Targeted Rewriting with {tactic}`conv` ）" =>
 
 
+:::comment
 The {tactic}`conv`, or conversion, tactic allows targeted rewriting within a goal.
 The argument to {tactic}`conv` is written in a separate language that interoperates with the main tactic language; it features commands to navigate to specific subterms within the goal along with commands that allow these subterms to be rewritten.
 {tactic}`conv` is useful when rewrites should only be applied in part of a goal (e.g. only on one side of an equality), rather than across the board, or when rewrites should be applied underneath a binder that prevents tactics like {tactic}`rw` from accessing the term.
 
+:::
+
+{tactic}`conv` 、もしくは変換タクティクはゴール内のターゲットを絞った書き換えを可能にします。 {tactic}`conv` の引数はメインのタクティク言語と相互に連携する別の言語で記述されます；これはゴール内の特定の部分項に移動するコマンドと、これらの部分項を書き換えるコマンドを備えています。 {tactic}`conv` は書き換えをゴール全体ではなく、ゴールの一部（例えば等式の片側のみ）にのみ適用する場合や、 {tactic}`rw` のようなタクティクが項にアクセスするのを防いでしまう束縛子の中の書き換えを適用する場合に便利です。
+
+:::comment
 The conversion tactic language is very similar to the main tactic language: it uses the same proof states, tactics work primarily on the main goal and may either fail or succeed with a sequence of new goals, and macro expansion is interleaved with tactic execution.
 Unlike the main tactic language, in which tactics are intended to eventually solve goals, the {tactic}`conv` tactic is used to _change_ a goal so that it becomes amenable to further processing in the main tactic language.
 Goals that are intended to be rewritten with {tactic}`conv` are shown with a vertical bar instead of a turnstile.
 
+:::
+
+変換タクティク言語はメインのタクティク言語に非常に似ています：同じ証明状態を使用し、タクティクは主にメインゴールに対して作用し、新しいゴールの列で失敗または成功する可能性があり、マクロ展開はタクティクの実行と交互に行われます。タクティクが最終的にゴールを解決するためのものであるメインのタクティク言語とは異なり、 {tactic}`conv` はゴールを _変更_ するために用いられます。これによってゴールはその後のメインのタクティク言語で容易に処理できるようになります。 {tactic}`conv` で書き換えることを意図しているゴールはターンスタイルの代わりに縦棒で表示されます。
+
 :::tactic "conv"
 :::
 
-::::example "Navigation and Rewriting with {tactic}`conv`"
+:::comment
+::example "Navigation and Rewriting with {tactic}`conv`"
+:::
+::::example "{tactic}`conv` による移動と書き換え"
 
+:::comment
 In this example, there are multiple instances of addition, and {tactic}`rw` would by default rewrite the first instance that it encounters.
 Using {tactic}`conv` to navigate to the specific subterm before rewriting leaves {tactic}`rw` no choice but to rewrite the correct term.
 
+:::
+
+この例では、加算のインスタンスが複数存在し、 {tactic}`rw` はデフォルトで最初に出会ったインスタンスを書き換えてしまいます。書き換える前に特定の部分項へ移動するために {tactic}`conv` を使用すると、 {tactic}`rw` は正しい項を書き換える以外に選択肢がなくなります。
+
 ```lean
 example (x y z : Nat) : x + (y + z) = (x + z) + y := by
   conv =>
@@ -47,13 +68,21 @@ example (x y z : Nat) : x + (y + z) = (x + z) + y := by
 
 ::::
 
-::::example "Rewriting Under Binders with {tactic}`conv`"
+:::comment
+::example "Rewriting Under Binders with {tactic}`conv`"
+:::
+::::example "{tactic}`conv` による束縛子の中の書き換え"
 
+:::comment
 In this example, addition occurs under binders, so {tactic}`rw` can't be used.
 However, after using {tactic}`conv` to navigate to the function body, it succeeds.
 The nested use of {tactic}`conv` causes control to return to the current position in the term after performing further coversions on one of its subterms.
 Because the goal is a reflexive equation after rewriting, {tactic}`conv` automatically closes it.
 
+:::
+
+この例では、加算は束縛子の中に存在するため、 {tactic}`rw` は使えません。しかし、 {tactic}`conv` を使用して関数本体に移動すると成功します。入れ子になった {tactic}`conv` の使用は、その部分項の1つに対してさらなる変換を実行したのち、制御を項の中の現在の位置に戻します。ゴールは書き換え後の反射性の等式であるため、 {tactic}`conv` は自動的にこれを閉じます。
+
 ```lean
 example : (fun (x y z : Nat) => x + (y + z)) = (fun x y z => (z + x) + y) := by
   conv =>
@@ -69,9 +98,14 @@ example : (fun (x y z : Nat) => x + (y + z)) = (fun x y z => (z + x) + y) := by
 
 ::::
 
+:::comment
 # Control Structures
 
 
+:::
+
+# 制御構造（Control Structures）
+
 :::conv first show := "first"
 :::
 
@@ -96,8 +130,13 @@ example : (fun (x y z : Nat) => x + (y + z)) = (fun x y z => (z + x) + y) := by
 :::conv convDone show:= "done"
 :::
 
+:::comment
 # Goal Selection
 
+:::
+
+# ゴールの選択（Goal Selection）
+
 :::conv allGoals show:= "all_goals"
 :::
 
@@ -126,8 +165,13 @@ example : (fun (x y z : Nat) => x + (y + z)) = (fun x y z => (z + x) + y) := by
 :::
 
 
+:::comment
 # Navigation
 
+:::
+
+# 移動（Navigation）
+
 :::conv lhs show:= "lhs"
 :::
 
@@ -177,9 +221,19 @@ $x:ident
 :::conv convIntro___ show := "intro"
 :::
 
+:::comment
 # Changing the Goal
+:::
+
+# ゴールの変更（Changing the Goal）
+
+:::comment
 ## Reduction
 
+:::
+
+## 簡約（Reduction）
+
 :::conv whnf show:= "whnf"
 :::
 
@@ -195,7 +249,12 @@ $x:ident
 :::conv unfold show:= "unfold"
 :::
 
+:::comment
 ## Simplification
+:::
+
+## 単純化（Simplification）
+
 :::conv simp show:= "simp"
 :::
 
@@ -205,9 +264,14 @@ $x:ident
 :::conv simpMatch show:= "simp_match"
 :::
 
+:::comment
 ## Rewriting
 
 
+:::
+
+## 書き換え（Rewriting）
+
 :::conv change show:= "change"
 :::
 
@@ -224,8 +288,13 @@ $x:ident
 :::
 
 
+:::comment
 # Nested Tactics
 
+:::
+
+# 入れ子のタクティク（Nested Tactics）
+
 :::tactic Lean.Parser.Tactic.Conv.convTactic
 :::
 
@@ -242,14 +311,24 @@ $x:ident
 :::
 
 
+:::comment
 # Debugging Utilities
 
+:::
+
+# デバッグ用ユーティリティ（Debugging Utilities）
+
 :::conv convTrace_state show:= "trace_state"
 :::
 
 
+:::comment
 # Other
 
+:::
+
+# その他（Other）
+
 :::conv convRfl show:= "rfl"
 :::