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.
- 9.1. Natural Numbers
- 9.2. Integers
- 9.3. Fixed-Precision Integer Types
- 9.4. Bitvectors
- 9.5. Floating-Point Numbers
- 9.6. Characters
-
9.7. Strings
- 9.7.1. Logical Model
- 9.7.2. Run-Time Representation
- 9.7.3. Syntax
-
9.7.4. API Reference
- 9.7.4.1. Constructing
- 9.7.4.2. Conversions
- 9.7.4.3. Properties
- 9.7.4.4. Positions
- 9.7.4.5. Lookups and Modifications
- 9.7.4.6. Folds and Aggregation
- 9.7.4.7. Comparisons
- 9.7.4.8. Manipulation
- 9.7.4.9. Iterators
- 9.7.4.10. Substrings
- 9.7.4.11. Proof Automation
- 9.7.4.12. Metaprogramming
- 9.7.4.13. Encodings
- 9.7.5. FFI
- 9.8. Linked Lists
- 9.9. Arrays
- 9.10. Lazy Computations
- 9.11. Tasks and Threads