←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.	Output from Lean
13.	Elan
14.	Lake and Reservoir
	Index

9. Basic Types

9.1.	Natural Numbers
9.2.	Integers
9.3.	Finite Natural Numbers
9.4.	Fixed-Precision Integer Types
9.5.	Bitvectors
9.6.	Floating-Point Numbers
9.7.	Characters
9.8.	Strings
9.9.	The Unit Type
9.10.	The Empty Type
9.11.	Booleans
9.12.	Optional Values
9.13.	Tuples
9.14.	Sum Types
9.15.	Linked Lists
9.16.	Arrays
9.17.	Subtypes
9.18.	Lazy Computations
9.19.	Tasks and Threads

9.5. Bitvectors

Source Code
Report Issues

9.5. Bitvectors🔗

Planned Content

Run-time and kernel representations of BitVec
API reference
Cross-reference to TBW chapter on bv_decide

Tracked at issue #106