Terms翻訳 (#42)

* 翻訳開始

* 翻訳完了

* 用語対応

Author: s-taiga

GLOSSARY.md

@@ -67,6 +67,7 @@
 | dependent type theory | 依存型理論 | |
 | derivation | 導出 | |
 | deriving | 導出 | |
+| destructure | 分解 | |
 | desugar | 脱糖 | |
 | diamond | ダイアモンド | 菱形継承問題関連の単語。菱形だとわかりづらいためカタカナにした |
 | discriminant | 判別子 | |
@@ -106,13 +107,15 @@
 | function extensionality | 関数外延性 | |
 | function type | 関数型 | |
 | gadget | ガジェット | |
+| generalized field notation | 一般化されたフィールド記法 | |
 | goal | ゴール | |
 | grammar | 文法 | |
 | guillemet | ギュメ | フランス語 |
 | heap region | ヒープ領域 | |
 | hierarchical identifier | 階層的識別子 | |
 | hierarchy | 階層 | |
 | higher-order function | 高階関数 | |
+| hole | ホール | |
 | hygiene | （マクロの）健全性 | |
 | hypothese | 仮定 | |
 | identically | 同一 | |
@@ -158,6 +161,7 @@
 | letter | 文字 | |
 | letterlike | 文字様 | |
 | level expression | レベル式 | |
+| lexical | レキシカル | |
 | longest match | 最長一致 | |
 | main goal | メインゴール | |
 | macro | マクロ | |
@@ -166,6 +170,8 @@
 | macro Expansion | マクロ展開 | |
 | map | 写像 | |
 | mapping | マッピング | |
+| match alternative | マッチ選択肢 | |
+| match discriminant | マッチ判別子 | |
 | measure | 測度 | 再帰関数で停止性を証明するために使用する項のこと。普通に「尺度」でも良さそう |
 | membership predicate | メンバシップ述語 | |
 | memoization | メモ化 | |
@@ -177,6 +183,7 @@
 | multi-threading | マルチスレッド | |
 | mutation | ミューテーション | |
 | mutually inductive | 相互帰納 | |
+| named arguments | 名前付き引数 | |
 | namespace | 名前空間 | |
 | nested | ネストされた | |
 | newline | 改行 | |
@@ -215,6 +222,7 @@
 | quotient type | 商型 | |
 | range | 値域 | |
 | raw identifier | 生識別子 | Rust By Exampleの表現を利用 |
+| realizing name | 名前実現 | |
 | reasoning | 推論 | |
 | recovery | 回復 | |
 | recursive-descent parser | 再帰下降パーサ | |
@@ -225,12 +233,14 @@
 | representation | 表現 | |
 | reserved keyword | 予約キーワード | 下のreserved wordの表記ゆれかもしれないがいったん別の訳語を割り当てる |
 | reserved word | 予約語 | |
+| resolving name | 名前解決 | |
 | rewrite | 書き換え | |
 | run-length encoding | 連長圧縮 | |
 | run-time | ランタイム | |
 | rule | 規則 | |
 | saturated application | 完全な適用 | 固定訳は無いように思われ、飽和では意味が分かりづらいため |
 | schematic definition | スキーマ的定義 | |
+| scientific literal | 科学的リテラル | |
 | scope | スコープ | |
 | scrutinee | 被検査対象 | |
 | separator | 区切り文字 | |
@@ -318,6 +328,7 @@
 | --- | --- |
 | choice node | |
 | cumulative | |
+| ellipsis | 他言語でも類似概念があるが、そちらでもそのまま英単語で表現されることが多そうだったため |
 | idiom bracket | https://wiki.haskell.org/Idiom_brackets |
 | impredicativity, predicativity | |
 | inhabited | |

Manual/Language.lean

@@ -274,7 +274,7 @@ The following data are tracked in section scopes:
 : The Current Namespace
 
   The {deftech}_current namespace_ is the namespace into which new declarations will be defined.
-  Additionally, {tech (key:="resolve")}[name resolution] includes all prefixes of the current namespace in the scope for global names.
+  Additionally, {tech (key:="解決")}[name resolution]resolve includes all prefixes of the current namespace in the scope for global names.
 
 : Opened Namespaces
 
@@ -287,7 +287,7 @@ The following data are tracked in section scopes:
 
 : Section Variables
 
-  {tech}[Section variables] are names (or {tech}[instance implicit] parameters) that are automatically added as parameters to definitions.
+  {tech}[Section variables] are names (or {tech}[インスタンス暗黙]instance implicit parameters) that are automatically added as parameters to definitions.
   They are also added as universally-quantified assumptions to theorems when they occur in the theorem's statement.
 
 

Manual/Language/Functions.lean

@@ -168,7 +168,7 @@ This information is used by the Lean elaborator, but it does not affect type che
 
 :::
 
-コア型理論には {tech}[implicit] パラメータはありませんが、関数型にはパラメータが暗黙かどうかの表示があります。この情報は Lean のエラボレータに使用されますが、コア型理論における型チェックや定義上の等価性には影響しないため、コア型理論についてだけ考える場合は無視しても構いません。
+コア型理論には {tech}[暗黙] パラメータはありませんが、関数型にはパラメータが暗黙かどうかの表示があります。この情報は Lean のエラボレータに使用されますが、コア型理論における型チェックや定義上の等価性には影響しないため、コア型理論についてだけ考える場合は無視しても構いません。
 
 :::comment
 ::example "Definitional Equality of Implicit and Explicit Function Types"

Manual/Language/RecursiveDefs/Structural.lean

@@ -424,7 +424,7 @@ This definition of {lean}`half` terminates, but this can't be checked by either
 This is because the gratuitous tuple in the {tech}[match discriminant] breaks the connection between {lean}`n` and the patterns that match it.
 :::
 
-この {lean}`half` の定義は停止しますが、これは構造的再帰でも十分な根拠のある再帰でもチェックできません。これは、 {tech}[match discriminant] の中にある不必要なタプルが {lean}`n` とそれにマッチするパターンとの間のつながりを壊してしまうからです。
+この {lean}`half` の定義は停止しますが、これは構造的再帰でも十分な根拠のある再帰でもチェックできません。これは、 {tech}[マッチ判別子] の中にある不必要なタプルが {lean}`n` とそれにマッチするパターンとの間のつながりを壊してしまうからです。
 
 ```lean (error := true) (name := badhalfmatch) (keep := false)
 def half (n : Nat) : Nat :=

Manual/Tactics.lean

@@ -567,7 +567,7 @@ Metavariables that result from tactics frequently appear as goals whose {tech}[c
 
 :::
 
-疑問符で始まる項は未知の値に対応する _メタ変数_ （metavariable）です。これらは {tech}[宇宙] レベルか項のいずれかを表すこともあります。メタ変数の中には、Lean のエラボレーションプロセスの一環として、値を決定するのに十分な情報が得られていないときに生じるものがあります。このようなメタ変数の名前の最後には `?m.392` や `?u.498` のように数字が付きます。その他のメタ変数はタクティクや {tech}[synthetic holes] の結果として存在するようになります。これらのメタ変数の名前には数字の要素はありません。タクティクの結果として生じるメタ変数は {tech}[ケースラベル] がメタ変数の名前と一致するゴールとして現れることが多いです。
+疑問符で始まる項は未知の値に対応する _メタ変数_ （metavariable）です。これらは {tech}[宇宙] レベルか項のいずれかを表すこともあります。メタ変数の中には、Lean のエラボレーションプロセスの一環として、値を決定するのに十分な情報が得られていないときに生じるものがあります。このようなメタ変数の名前の最後には `?m.392` や `?u.498` のように数字が付きます。その他のメタ変数はタクティクや {tech}[統合的ホール] の結果として存在するようになります。これらのメタ変数の名前には数字の要素はありません。タクティクの結果として生じるメタ変数は {tech}[ケースラベル] がメタ変数の名前と一致するゴールとして現れることが多いです。
 
 :::comment
 ::example "Universe Level Metavariables"
@@ -1185,7 +1185,7 @@ Variable references in tactic scripts refer either to names that were in scope a
 
 :::
 
-Lean のタクティク言語は _健全_ {index subterm := "in tactics"}[hygiene] （hygienic）です。これはタクティク言語が字句スコープを尊重することを意味します：タクティク内で出現する名前は生成されたコードによって決定されるのではなく、ソースコードの束縛を参照しており、タクティクフレームワークはこのプロパティを維持する責任があります。タクティクスクリプトの変数参照は裏側で証明項で使うために選ばれた名前ではなく、スクリプトの最初にスコープにあった名前か、タクティクの一部として明示的に導入された束縛を参照します。
+Lean のタクティク言語は _健全_ {index subterm := "in tactics"}[hygiene] （hygienic）です。これはタクティク言語がレキシカルスコープを尊重することを意味します：タクティク内で出現する名前は生成されたコードによって決定されるのではなく、ソースコードの束縛を参照しており、タクティクフレームワークはこのプロパティを維持する責任があります。タクティクスクリプトの変数参照は裏側で証明項で使うために選ばれた名前ではなく、スクリプトの最初にスコープにあった名前か、タクティクの一部として明示的に導入された束縛を参照します。
 
 :::comment
 A consequence of hygienic tactics is that the only way to refer to an assumption is to explicitly name it.