←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

11. Notations and Macros

11.1.	Notations
11.2.	Syntax Categories and Extensions
11.3.	Macros
11.4.	Elaborators

11.1. Notations

Source Code
Report Issues

11.1. Notations🔗

Planned Content

A presentation of the notation command and how to define infix operators

Tracked at issue #69