13. 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. 13.1. Natural Numbers
    1. 13.1.1. Logical Model
    2. 13.1.2. Run-Time Representation
      1. 13.1.2.1. Performance Notes
    3. 13.1.3. Syntax
    4. 13.1.4. API Reference
      1. 13.1.4.1. Arithmetic
        1. 13.1.4.1.1. Bitwise Operations
      2. 13.1.4.2. Minimum and Maximum
      3. 13.1.4.3. GCD and LCM
      4. 13.1.4.4. Powers of Two
      5. 13.1.4.5. Comparisons
        1. 13.1.4.5.1. Boolean Comparisons
        2. 13.1.4.5.2. Decidable Equality
        3. 13.1.4.5.3. Predicates
      6. 13.1.4.6. Iteration
      7. 13.1.4.7. Conversion
        1. 13.1.4.7.1. Metaprogramming and Internals
      8. 13.1.4.8. Elimination
        1. 13.1.4.8.1. Alternative Induction Principles
    5. 13.1.5. Simplification
  2. 13.2. Integers
    1. 13.2.1. Logical Model
    2. 13.2.2. Run-Time Representation
    3. 13.2.3. Syntax
    4. 13.2.4. API Reference
      1. 13.2.4.1. Properties
      2. 13.2.4.2. Conversions
      3. 13.2.4.3. Arithmetic
        1. 13.2.4.3.1. Division
      4. 13.2.4.4. Bitwise Operators
      5. 13.2.4.5. Comparisons
      6. 13.2.4.6. Proof Automation
  3. 13.3. Finite Natural Numbers
    1. 13.3.1. Run-Time Characteristics
    2. 13.3.2. Coercions and Literals
    3. 13.3.3. API Reference
      1. 13.3.3.1. Construction
      2. 13.3.3.2. Arithmetic
      3. 13.3.3.3. Bitwise Operations
      4. 13.3.3.4. Conversions
      5. 13.3.3.5. Iteration
      6. 13.3.3.6. Reasoning
      7. 13.3.3.7. Proof Automation
  4. 13.4. Fixed-Precision Integer Types
    1. 13.4.1. Logical Model
      1. 13.4.1.1. Unsigned
      2. 13.4.1.2. Signed
    2. 13.4.2. Run-Time Representation
    3. 13.4.3. Syntax
    4. 13.4.4. API Reference
      1. 13.4.4.1. Sizes
      2. 13.4.4.2. Conversions
        1. 13.4.4.2.1. To and From Int
        2. 13.4.4.2.2. To and From Nat
        3. 13.4.4.2.3. To Other Fixed-Width Integers
        4. 13.4.4.2.4. To Floating-Point Numbers
        5. 13.4.4.2.5. To Bitvectors
        6. 13.4.4.2.6. To Finite Numbers
        7. 13.4.4.2.7. To Characters
      3. 13.4.4.3. Comparisons
      4. 13.4.4.4. Arithmetic
      5. 13.4.4.5. Bitwise Operations
      6. 13.4.4.6. Proof Automation
  5. 13.5. Bitvectors
  6. 13.6. Floating-Point Numbers
  7. 13.7. Characters
    1. 13.7.1. Syntax
    2. 13.7.2. Logical Model
    3. 13.7.3. Run-Time Representation
    4. 13.7.4. API Reference
      1. 13.7.4.1. Character Classes
  8. 13.8. Strings
    1. 13.8.1. Logical Model
    2. 13.8.2. Run-Time Representation
      1. 13.8.2.1. Performance Notes
    3. 13.8.3. Syntax
      1. 13.8.3.1. String Literals
      2. 13.8.3.2. Interpolated Strings
      3. 13.8.3.3. Raw String Literals
    4. 13.8.4. API Reference
      1. 13.8.4.1. Constructing
      2. 13.8.4.2. Conversions
      3. 13.8.4.3. Properties
      4. 13.8.4.4. Positions
      5. 13.8.4.5. Lookups and Modifications
      6. 13.8.4.6. Folds and Aggregation
      7. 13.8.4.7. Comparisons
      8. 13.8.4.8. Manipulation
      9. 13.8.4.9. Iterators
      10. 13.8.4.10. Substrings
      11. 13.8.4.11. Proof Automation
      12. 13.8.4.12. Metaprogramming
      13. 13.8.4.13. Encodings
    5. 13.8.5. FFI
  9. 13.9. The Unit Type
    1. 13.9.1. Definitional Equality
  10. 13.10. The Empty Type
    1. 13.10.1. API Reference
  11. 13.11. Booleans
    1. 13.11.1. Run-Time Representation
    2. 13.11.2. Booleans and Propositions
    3. 13.11.3. Syntax
    4. 13.11.4. API Reference
      1. 13.11.4.1. Logical Operations
      2. 13.11.4.2. Comparisons
      3. 13.11.4.3. Conversions
  12. 13.12. Optional Values
    1. 13.12.1. Coercions
    2. 13.12.2. API Reference
      1. 13.12.2.1. Extracting Values
      2. 13.12.2.2. Properties and Comparisons
      3. 13.12.2.3. Conversion
      4. 13.12.2.4. Control
      5. 13.12.2.5. Iteration
      6. 13.12.2.6. Recursion Helpers
      7. 13.12.2.7. Reasoning
  13. 13.13. Tuples
    1. 13.13.1. Ordered Pairs
      1. 13.13.1.1. API Reference
        1. 13.13.1.1.1. Ordering
        2. 13.13.1.1.2. Transformation
        3. 13.13.1.1.3. Natural Number Ranges
    2. 13.13.2. Dependent Pairs
  14. 13.14. Sum Types
    1. 13.14.1. Syntax
    2. 13.14.2. API Reference
      1. 13.14.2.1. Case Distinction
      2. 13.14.2.2. Extracting Values
      3. 13.14.2.3. Transformations
      4. 13.14.2.4. Inhabited
  15. 13.15. Linked Lists
    1. 13.15.1. Syntax
    2. 13.15.2. Performance Notes
    3. 13.15.3. API Reference
      1. 13.15.3.1. Predicates and Relations
      2. 13.15.3.2. Constructing Lists
      3. 13.15.3.3. Length
      4. 13.15.3.4. Head and Tail
      5. 13.15.3.5. Lookups
        1. 13.15.3.5.1. Queries
      6. 13.15.3.6. Conversions
      7. 13.15.3.7. Modification
        1. 13.15.3.7.1. Insertion
      8. 13.15.3.8. Sorting
      9. 13.15.3.9. Iteration
        1. 13.15.3.9.1. Folds
      10. 13.15.3.10. Transformation
      11. 13.15.3.11. Filtering
      12. 13.15.3.12. Partitioning
      13. 13.15.3.13. Element Predicates
      14. 13.15.3.14. Comparisons
      15. 13.15.3.15. Termination Helpers
      16. 13.15.3.16. Proof Automation
  16. 13.16. Arrays
    1. 13.16.1. Logical Model
    2. 13.16.2. Run-Time Representation
      1. 13.16.2.1. Performance Notes
    3. 13.16.3. Syntax
    4. 13.16.4. API Reference
      1. 13.16.4.1. Constructing Arrays
      2. 13.16.4.2. Size
      3. 13.16.4.3. Lookups
      4. 13.16.4.4. Conversions
      5. 13.16.4.5. Modification
      6. 13.16.4.6. Sorted Arrays
      7. 13.16.4.7. Iteration
      8. 13.16.4.8. Transformation
      9. 13.16.4.9. Filtering
      10. 13.16.4.10. Partitioning
      11. 13.16.4.11. Element Predicates
      12. 13.16.4.12. Comparisons
      13. 13.16.4.13. Termination Helpers
      14. 13.16.4.14. Proof Automation
    5. 13.16.5. Sub-Arrays
      1. 13.16.5.1. Size
      2. 13.16.5.2. Resizing
      3. 13.16.5.3. Lookups
      4. 13.16.5.4. Iteration
      5. 13.16.5.5. Element Predicates
    6. 13.16.6. FFI
  17. 13.17. Subtypes
  18. 13.18. Lazy Computations
  19. 13.19. Tasks and Threads