←Prev ↑Up Next→

The Lean Language Reference

1.	Introduction
2.	Elaboration and Compilation
3.	The Lean Language
4.	Terms
5.	Monads and `do`-Notation
6.	IO
7.	Tactic Proofs
8.	The Simplifier
9.	Basic Types
10.	Standard Library
11.	Notations and Macros
12.	Elan
13.	Lake and Reservoir
	Index

9. Basic Types

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.8.	Linked Lists
9.9.	Arrays
9.10.	Lazy Computations
9.11.	Tasks and Threads

9.5. Floating-Point Numbers

9.5. Floating-Point Numbers

Planned Content

Run-time and kernel representations
Precision, and whether it's platform-dependent
Relationship between IEEE floats and decidable equality

Tracked at issue #107