The Lean Language Reference

The Lean Language Reference

Table of Contents

1.	Introduction
2.	Elaboration and Compilation
3.	Interacting with Lean
4.	The Type System
5.	Source Files and Modules
6.	Namespaces and Sections
7.	Definitions
8.	Axioms
9.	Attributes
10.	Type Classes
11.	Coercions
12.	Run-Time Code
13.	Terms
14.	Tactic Proofs
15.	The Simplifier
16.	The `grind` tactic
17.	The `mvcgen` tactic
18.	Functors, Monads and `do`-Notation
19.	Basic Propositions
20.	Basic Types
21.	IO
22.	Iterators
23.	Notations and Macros
24.	Build Tools and Distribution
	Validating a Lean Proof
	Error Explanations
	Release Notes
	Supported Platforms
	Index

13. Terms

13.1.	Identifiers
13.2.	Function Types
13.3.	Functions
13.4.	Function Application
13.5.	Numeric Literals
13.6.	Structures and Constructors
13.7.	Conditionals
13.8.	Pattern Matching
13.9.	Holes
13.10.	Type Ascription
13.11.	Quotation and Antiquotation
13.12.	`do`-Notation
13.13.	Proofs

13.6. Structures and Constructors

Source Code
Report Issues

←13.5. Numeric Literals 13.7. Conditionals→

13.6. Structures and Constructors🔗

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

←13.5. Numeric Literals 13.7. Conditionals→