←Prev ↑UpNext→

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

11. Notations and Macros

11.1.	Custom Operators
11.2.	Precedence
11.3.	Notations
11.4.	Defining New Syntax
11.5.	Macros
11.6.	Elaborators

11.6. Elaborators

Source Code
Report Issues

11.6. Elaborators🔗

Planned Content

For now, a quick overview of term and command elaborators, with a detailed description to be written in a later revision.

Tracked at issue #72