12. 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. 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 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. 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 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. Raw String Literals
    4. 12.8.4. 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 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 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