←Prev ↑Up Next→

The Lean Language Reference

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

7. Terms

7.1.	Identifiers
7.2.	Function Types
7.3.	Functions
7.4.	Function Application
7.5.	Literals
7.6.	Structures and Constructors
7.7.	Conditionals
7.8.	Pattern Matching
7.9.	Holes
7.10.	Type Ascription
7.11.	Quotation and Antiquotation
7.12.	`do`-Notation
7.13.	Proofs

7.6. Structures and Constructors

Source Code
Report Issues

7.6. Structures and Constructors

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