←Prev ↑Up Next→

The Lean Language Reference

1.	Introduction
2.	Elaboration and Compilation
3.	The Type System
4.	Source Files
5.	Terms
6.	Type Classes
7.	Functors, Monads and `do`-Notation
8.	IO
9.	Tactic Proofs
10.	The Simplifier
11.	Basic Types
12.	Standard Library
13.	Notations and Macros
14.	Output from Lean
15.	Elan
16.	Lake and Reservoir
	Index

5. Terms

5.1.	Identifiers
5.2.	Function Types
5.3.	Functions
5.4.	Function Application
5.5.	Literals
5.6.	Structures and Constructors
5.7.	Conditionals
5.8.	Pattern Matching
5.9.	Holes
5.10.	Type Ascription
5.11.	Quotation and Antiquotation
5.12.	`do`-Notation
5.13.	Proofs

5.6. Structures and Constructors

Source Code
Report Issues

5.6. Structures and Constructors

Anonymous constructors and structure instance syntax are described in their respective sections.