9. Basic Types🔗

Lean includes a number of built-in types 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
  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 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. Raw String Literals
    4. 9.7.4. 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. The Unit Type
    1. 9.8.1. Definitional Equality
  9. 9.9. Booleans
  10. 9.10. Linked Lists
  11. 9.11. Arrays
    1. 9.11.1. Logical Model
    2. 9.11.2. Run-Time Representation
      1. 9.11.2.1. Performance Notes
    3. 9.11.3. Syntax
    4. 9.11.4. API Reference
      1. 9.11.4.1. Constructing Arrays
      2. 9.11.4.2. Size
      3. 9.11.4.3. Lookups
      4. 9.11.4.4. Conversions
      5. 9.11.4.5. Modification
      6. 9.11.4.6. Sorted Arrays
      7. 9.11.4.7. Iteration
      8. 9.11.4.8. Transformation
      9. 9.11.4.9. Filtering
      10. 9.11.4.10. Partitioning
      11. 9.11.4.11. Element Predicates
      12. 9.11.4.12. Comparisons
      13. 9.11.4.13. Termination Helpers
      14. 9.11.4.14. Proof Automation
    5. 9.11.5. Sub-Arrays
      1. 9.11.5.1. Size
      2. 9.11.5.2. Resizing
      3. 9.11.5.3. Lookups
      4. 9.11.5.4. Iteration
      5. 9.11.5.5. Element Predicates
    6. 9.11.6. FFI
  12. 9.12. Lazy Computations
  13. 9.13. Tasks and Threads