1.	Introduction
2.	Elaboration and Compilation
3.	The Lean Language
4.	Terms
5.	Functors, 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

4. Terms

4.1.	Identifiers
4.2.	Function Types
4.3.	Functions
4.4.	Function Application
4.5.	Literals
4.6.	Structures and Constructors
4.7.	Conditionals
4.8.	Pattern Matching
4.9.	Holes
4.10.	Type Ascription
4.11.	Quotation and Antiquotation
4.12.	`do`-Notation
4.13.	Proofs

4.11. Quotation and Antiquotation

Quotation terms are described in the section on quotation.