←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.	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.8. Linked Lists

Source Code
Report Issues

9.8. Linked Lists🔗

Planned Content

Representation at compile time and run time
API reference
Literal syntax
Constructor/pattern syntax

Tracked at issue #108