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

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

  1. 9.1. 自然数（Natural Numbers）
    1. 9.1.1. 論理モデル（Logical Model）
    2. 9.1.2. Run-Time Representation
      1. 9.1.2.1. パフォーマンスについての注記（Performance Notes）
    3. 9.1.3. 構文（Syntax）
    4. 9.1.4. API リファレンス（API Reference）
      1. 9.1.4.1. 算術（Arithmetic）
        1. 9.1.4.1.1. ビット演算（Bitwise Operations）
      2. 9.1.4.2. 最小・最大（Minimum and Maximum）
      3. 9.1.4.3. 最大公約数と最小公倍数（GCD and LCM）
      4. 9.1.4.4. 2の累乗（Powers of Two）
      5. 9.1.4.5. 比較（Comparisons）
        1. 9.1.4.5.1. 真偽値の比較（Boolean Comparisons）
        2. 9.1.4.5.2. 決定的な等価性（Decidable Equality）
        3. 9.1.4.5.3. 述語（Predicates）
      6. 9.1.4.6. 反復（Iteration）
      7. 9.1.4.7. 変換（Conversion）
        1. 9.1.4.7.1. メタプログラミングと内部（Metaprogramming and Internals）
      8. 9.1.4.8. キャスト（Casts）
      9. 9.1.4.9. 除去（Elimination）
        1. 9.1.4.9.1. 代替の帰納原理（Alternative Induction Principles）
    5. 9.1.5. 単純化（Simplification）
  2. 9.2. Integers
  3. 9.3. Fixed-Precision Integer Types
  4. 9.4. Bitvectors
  5. 9.5. Floating-Point Numbers
  6. 9.6. 文字（Characters）
    1. 9.6.1. 構文（Syntax）
    2. 9.6.2. 論理モデル（Logical Model）
    3. 9.6.3. ランタイム表現（Run-Time Representation）
    4. 9.6.4. API リファレンス（API Reference）
      1. 9.6.4.1. 文字クラス（Character Classes）
  7. 9.7. 文字列（Strings）
    1. 9.7.1. 論理モデル（Logical Model）
    2. 9.7.2. ランタイム表現（Run-Time Representation）
      1. 9.7.2.1. パフォーマンスについての注記（Performance Notes）
    3. 9.7.3. 構文（Syntax）
      1. 9.7.3.1. 文字列リテラル（String Literals）
      2. 9.7.3.2. 補間文字列（Interpolated Strings）
      3. 9.7.3.3. 生文字列リテラル
    4. 9.7.4. API リファレンス（API Reference）
      1. 9.7.4.1. 構成（Constructing）
      2. 9.7.4.2. 変換（Conversions）
      3. 9.7.4.3. プロパティ（Properties）
      4. 9.7.4.4. 位置（Positions）
      5. 9.7.4.5. 検索と変更（Lookups and Modifications）
      6. 9.7.4.6. 畳み込みと集約（Folds and Aggregation）
      7. 9.7.4.7. 比較（Comparisons）
      8. 9.7.4.8. 操作（Manipulation）
      9. 9.7.4.9. イテレータ（Iterators）
      10. 9.7.4.10. 部分文字列（Substrings）
      11. 9.7.4.11. 証明自動化（Proof Automation）
      12. 9.7.4.12. メタプログラミング（Metaprogramming）
      13. 9.7.4.13. エンコード（Encodings）
    5. 9.7.5. FFI
  8. 9.8. Linked Lists
  9. 9.9. Arrays
    1. 9.9.1. Logical Model
    2. 9.9.2. Run-Time Representation
      1. 9.9.2.1. Performance Notes
    3. 9.9.3. Syntax
    4. 9.9.4. API Reference
      1. 9.9.4.1. Constructing Arrays
      2. 9.9.4.2. Size
      3. 9.9.4.3. Lookups
      4. 9.9.4.4. Conversions
      5. 9.9.4.5. Modification
      6. 9.9.4.6. Sorted Arrays
      7. 9.9.4.7. Iteration
      8. 9.9.4.8. Transformation
      9. 9.9.4.9. Filtering
      10. 9.9.4.10. Partitioning
      11. 9.9.4.11. Element Predicates
      12. 9.9.4.12. Comparisons
      13. 9.9.4.13. Termination Helpers
      14. 9.9.4.14. Proof Automation
    5. 9.9.5. Sub-Arrays
      1. 9.9.5.1. Size
      2. 9.9.5.2. Resizing
      3. 9.9.5.3. Lookups
      4. 9.9.5.4. Iteration
      5. 9.9.5.5. Element Predicates
    6. 9.9.6. FFI
  10. 9.10. Lazy Computations
  11. 9.11. Tasks and Threads