12. 基本的な型（Basic Types）🔗

Lean にはコンパイラが特別にサポートする組み込みの型が多数あります。 Nat のように、カーネルで特別にサポートされているものもあります。その他の型はコンパイラからの特別なサポート 自体 はありませんが、パフォーマンス上の理由から型の内部表現に依存しています。

1. 12.1. 自然数（Natural Numbers）
   1. 12.1.1. 論理モデル（Logical Model）
   2. 12.1.2. ランタイム表現（Run-Time Representation）
      1. 12.1.2.1. パフォーマンスについての注記（Performance Notes）
   3. 12.1.3. 構文（Syntax）
   4. 12.1.4. API リファレンス（API Reference）
      1. 12.1.4.1. 算術（Arithmetic）
         1. 12.1.4.1.1. ビット演算（Bitwise Operations）
      2. 12.1.4.2. 最小・最大（Minimum and Maximum）
      3. 12.1.4.3. 最大公約数と最小公倍数（GCD and LCM）
      4. 12.1.4.4. 2の累乗（Powers of Two）
      5. 12.1.4.5. 比較（Comparisons）
         1. 12.1.4.5.1. 真偽値の比較（Boolean Comparisons）
         2. 12.1.4.5.2. 決定的な等価性（Decidable Equality）
         3. 12.1.4.5.3. 述語（Predicates）
      6. 12.1.4.6. 反復（Iteration）
      7. 12.1.4.7. 変換（Conversion）
         1. 12.1.4.7.1. メタプログラミングと内部（Metaprogramming and Internals）
      8. 12.1.4.8. キャスト（Casts）
      9. 12.1.4.9. 除去（Elimination）
         1. 12.1.4.9.1. 代替の帰納原理（Alternative Induction Principles）
   5. 12.1.5. 単純化（Simplification）
2. 12.2. Integers
   1. 12.2.1. Logical Model
   2. 12.2.2. Run-Time Representation
   3. 12.2.3. Syntax
   4. 12.2.4. API Reference
      1. 12.2.4.1. Properties
      2. 12.2.4.2. Conversions
         1. 12.2.4.2.1. Casts
      3. 12.2.4.3. Arithmetic
         1. 12.2.4.3.1. Division
      4. 12.2.4.4. Bitwise Operators
      5. 12.2.4.5. Comparisons
      6. 12.2.4.6. Proof Automation
3. 12.3. Finite Natural Numbers
   1. 12.3.1. Run-Time Characteristics
   2. 12.3.2. Coercions and Literals
   3. 12.3.3. API Reference
      1. 12.3.3.1. Construction
      2. 12.3.3.2. Arithmetic
      3. 12.3.3.3. Bitwise Operations
      4. 12.3.3.4. Conversions
      5. 12.3.3.5. Iteration
      6. 12.3.3.6. Reasoning
      7. 12.3.3.7. Proof Automation
4. 12.4. Fixed-Precision Integer Types
   1. 12.4.1. Logical Model
      1. 12.4.1.1. Unsigned
      2. 12.4.1.2. Signed
   2. 12.4.2. Run-Time Representation
   3. 12.4.3. Syntax
   4. 12.4.4. API Reference
      1. 12.4.4.1. Sizes
      2. 12.4.4.2. Conversions
         1. 12.4.4.2.1. To and From Int
         2. 12.4.4.2.2. To and From Nat
         3. 12.4.4.2.3. To Other Fixed-Width Integers
         4. 12.4.4.2.4. To Floating-Point Numbers
         5. 12.4.4.2.5. To Bitvectors
         6. 12.4.4.2.6. To Finite Numbers
         7. 12.4.4.2.7. To Characters
      3. 12.4.4.3. Comparisons
      4. 12.4.4.4. Arithmetic
      5. 12.4.4.5. Bitwise Operations
      6. 12.4.4.6. Proof Automation
5. 12.5. Bitvectors
6. 12.6. Floating-Point Numbers
7. 12.7. 文字（Characters）
   1. 12.7.1. 構文（Syntax）
   2. 12.7.2. 論理モデル（Logical Model）
   3. 12.7.3. ランタイム表現（Run-Time Representation）
   4. 12.7.4. API リファレンス（API Reference）
      1. 12.7.4.1. 文字クラス（Character Classes）
8. 12.8. 文字列（Strings）
   1. 12.8.1. 論理モデル（Logical Model）
   2. 12.8.2. ランタイム表現（Run-Time Representation）
      1. 12.8.2.1. パフォーマンスについての注記（Performance Notes）
   3. 12.8.3. 構文（Syntax）
      1. 12.8.3.1. 文字列リテラル（String Literals）
      2. 12.8.3.2. 補間文字列（Interpolated Strings）
      3. 12.8.3.3. 生文字列リテラル
   4. 12.8.4. API リファレンス（API Reference）
      1. 12.8.4.1. 構成（Constructing）
      2. 12.8.4.2. 変換（Conversions）
      3. 12.8.4.3. プロパティ（Properties）
      4. 12.8.4.4. 位置（Positions）
      5. 12.8.4.5. 検索と変更（Lookups and Modifications）
      6. 12.8.4.6. 畳み込みと集約（Folds and Aggregation）
      7. 12.8.4.7. 比較（Comparisons）
      8. 12.8.4.8. 操作（Manipulation）
      9. 12.8.4.9. イテレータ（Iterators）
      10. 12.8.4.10. 部分文字列（Substrings）
      11. 12.8.4.11. 証明自動化（Proof Automation）
      12. 12.8.4.12. メタプログラミング（Metaprogramming）
      13. 12.8.4.13. エンコード（Encodings）
   5. 12.8.5. FFI
9. 12.9. ユニット型（The Unit Type）
   1. 12.9.1. Definitional Equality
10. 12.10. The Empty Type
    1. 12.10.1. API Reference
11. 12.11. 真偽値（Booleans）
    1. 12.11.1. ランタイム表現（Run-Time Representation）
    2. 12.11.2. 真偽値と命題（Booleans and Propositions）
    3. 12.11.3. 構文（Syntax）
    4. 12.11.4. API リファレンス（API Reference）
       1. 12.11.4.1. 論理演算子（Logical Operations）
       2. 12.11.4.2. 比較（Comparisons）
       3. 12.11.4.3. 変換（Conversions）
12. 12.12. Optional Values
    1. 12.12.1. Coercions
    2. 12.12.2. API Reference
       1. 12.12.2.1. Extracting Values
       2. 12.12.2.2. Properties and Comparisons
       3. 12.12.2.3. Conversion
       4. 12.12.2.4. Control
       5. 12.12.2.5. Iteration
       6. 12.12.2.6. Recursion Helpers
       7. 12.12.2.7. Reasoning
13. 12.13. Tuples
14. 12.14. Sum Types
15. 12.15. Dependent Pairs
16. 12.16. Linked Lists
17. 12.17. 配列（Arrays）
    1. 12.17.1. 論理モデル（Logical Model）
    2. 12.17.2. ランタイム表現（Run-Time Representation）
       1. 12.17.2.1. パフォーマンスについての注記（Performance Notes）
    3. 12.17.3. 構文（Syntax）
    4. 12.17.4. API リファレンス（API Reference）
       1. 12.17.4.1. 配列の構成（Constructing Arrays）
       2. 12.17.4.2. サイズ（Size）
       3. 12.17.4.3. 検索（Lookups）
       4. 12.17.4.4. 別の型への変換（Conversions）
       5. 12.17.4.5. 配列の変更（Modification）
       6. 12.17.4.6. 配列のソート（Sorted Arrays）
       7. 12.17.4.7. 反復（Iteration）
       8. 12.17.4.8. 要素の変換（Transformation）
       9. 12.17.4.9. フィルタ（Filtering）
       10. 12.17.4.10. 分割（Partitioning）
       11. 12.17.4.11. 要素についての述語（Element Predicates）
       12. 12.17.4.12. 比較（Comparisons）
       13. 12.17.4.13. Termination Helpers
       14. 12.17.4.14. 証明の自動化（Proof Automation）
    5. 12.17.5. 部分配列（Sub-Arrays）
       1. 12.17.5.1. サイズ（Size）
       2. 12.17.5.2. サイズ変更（Resizing）
       3. 12.17.5.3. 検索（Lookups）
       4. 12.17.5.4. 反復（Iteration）
       5. 12.17.5.5. 要素についての述語（Element Predicates）
    6. 12.17.6. FFI
18. 12.18. Subtypes
19. 12.19. Lazy Computations
20. 12.20. Tasks and Threads