20. 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.
- 20.1. Natural Numbers
- 20.2. Integers
- 20.3. Finite Natural Numbers
- 20.4. Fixed-Precision Integers
- 20.5. Bitvectors
- 20.6. Floating-Point Numbers
- 20.7. Characters
- 20.8. Strings
- 20.9. The Unit Type
- 20.10. The Empty Type
- 20.11. Booleans
- 20.12. Optional Values
- 20.13. Tuples
- 20.14. Sum Types
- 20.15. Linked Lists
- 20.16. Arrays
- 20.17. Maps and Sets
- 20.18. Subtypes
- 20.19. Lazy Computations