9. Basic Types

Lean includes a number of built-in datatypes that are specially supported by the compiler. Some, such as 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.

  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 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. 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
      1. 9.1.5.1. Normal Form
      2. 9.1.5.2. Helpers
  2. 9.2. Integers
  3. 9.3. Fixed-Precision Integer Types
  4. 9.4. Floating-Point Numbers
  5. 9.5. Characters
    1. 9.5.1. Syntax
    2. 9.5.2. Logical Model
    3. 9.5.3. Run-Time Representation
    4. 9.5.4. API Reference
      1. 9.5.4.1. Character Classes
  6. 9.6. Strings
    1. 9.6.1. Logical Model
    2. 9.6.2. Run-Time Representation
      1. 9.6.2.1. Performance Notes
    3. 9.6.3. Syntax
      1. 9.6.3.1. String Literals
      2. 9.6.3.2. Interpolated Strings
      3. 9.6.3.3. Raw String Literals
    4. 9.6.4. API Reference
      1. 9.6.4.1. Constructing
      2. 9.6.4.2. Conversions
      3. 9.6.4.3. Properties
      4. 9.6.4.4. Positions
      5. 9.6.4.5. Lookups and Modifications
      6. 9.6.4.6. Folds and Aggregation
      7. 9.6.4.7. Comparisons
      8. 9.6.4.8. Manipulation
      9. 9.6.4.9. Iterators
      10. 9.6.4.10. Substrings
      11. 9.6.4.11. Proof Automation
      12. 9.6.4.12. Metaprogramming
      13. 9.6.4.13. Encodings
    5. 9.6.5. FFI
  7. 9.7. Linked Lists
  8. 9.8. Arrays
  9. 9.9. Lazy Computations
  10. 9.10. Tasks and Threads