BasicTypes翻訳 (#15)

* 翻訳開始

* 翻訳完了

Author: s-taiga

GLOSSARY.md

@@ -111,6 +111,7 @@
 | identifier component | 識別子要素 | |
 | identifier continuation character | 識別子継続文字 | |
 | identity function | 恒等関数 | |
+| immediate value | 即値 | |
 | imperative | 命令型 | |
 | implicit parameter | 暗黙のパラメータ | |
 | inaccessible | （仮定のアクセス可否の文脈で）アクセス不能 | |
@@ -134,6 +135,7 @@
 | interface | インタフェース | |
 | interleave | 交互に実行する | |
 | intermediate representation | 中間表現 | |
+| interpolate | 補間 | |
 | invariant | 不変量 | |
 | kernel | カーネル | |
 | keyword | キーワード | |
@@ -289,6 +291,7 @@
 | choice node | |
 | cumulative | |
 | impredicativity, predicativity | |
+| no confusion | |
 | packed array | System Verilogという言語にこの名前の文法要素がある？ |
 | strict positively, negatively | 自己言及される定義の分類、定訳は無い模様 |
 | prelude | |

Manual/BasicTypes.lean

@@ -18,16 +18,24 @@ open Verso.Genre Manual
 set_option pp.rawOnError true
 
 
+/-
 #doc (Manual) "Basic Types" =>
+-/
+#doc (Manual) "基本的な型（Basic Types）" =>
 %%%
 tag := "basic-types"
 %%%
 
 
+:::comment
 Lean includes a number of built-in types that are specially supported by the compiler.
 Some, such as {lean}`Nat`, additionally have special support in the kernel.
 Other types don't have special compiler support _per se_, but rely in important ways on the internal representation of types for performance reasons.
 
+:::
+
+Lean にはコンパイラが特別にサポートする組み込みの型が多数あります。 {lean}`Nat` のように、カーネルで特別にサポートされているものもあります。その他の型はコンパイラからの特別なサポート _自体_ はありませんが、パフォーマンス上の理由から型の内部表現に依存しています。
+
 {include 0 Manual.BasicTypes.Nat}
 
 # Integers
@@ -106,46 +114,80 @@ tag := "Float"
  * Relationship between IEEE floats and decidable equality
 :::
 
+:::comment
 # Characters
 %%%
 tag := "Char"
 %%%
 
 
+:::
+
+# 文字（Characters）
+
 {docstring Char}
 
+:::comment
 ## Syntax
 %%%
 tag := "char-syntax"
 %%%
 
 
+:::
+
+## 構文（Syntax）
+
+:::comment
 ## Logical Model
 %%%
 tag := "char-model"
 %%%
 
+:::
+
+## 論理モデル（Logical Model）
+
+:::comment
 ## 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 {lean}`Char` does not require indirection to access. In polymorphic contexts, characters are boxed.
 
 
+:::
+
+モノ射なコンテキストでは、文字は32ビットの即値として表現されます。言い換えると、{lean}`Char` 型のコンストラクタや構造体のフィールドにアクセスする際にインダイレクトは必要ありません。多相なコンテキストでは文字はボックス化されます。
+
+:::comment
 ## API Reference
 %%%
 tag := "char-api"
 %%%
 
 
+:::
+
+## API リファレンス（API Reference）
+
+:::comment
 ### Character Classes
 %%%
 tag := "char-api-classes"
 %%%
 
 
+:::
+
+### 文字クラス（Character Classes）
+
 {docstring Char.isAlpha}
 
 {docstring Char.isAlphanum}