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.	Terms
11.	Type Classes
12.	Coercions
13.	Tactic Proofs
14.	Functors, Monads and `do`-Notation
15.	IO
16.	The Simplifier
17.	The `grind` tactic
18.	The `mvcgen` tactic
19.	Basic Propositions
20.	Basic Types
21.	Dynamic Typing
22.	Standard Library
23.	Notations and Macros
24.	Run-Time Code
25.	Build Tools and Distribution
	Error Explanations
	The Module System
	Release Notes
	Index
	Progress

10. Terms

10.1.	Identifiers
10.2.	Function Types
10.3.	Functions
10.4.	Function Application
10.5.	Numeric Literals
10.6.	Structures and Constructors
10.7.	Conditionals
10.8.	Pattern Matching
10.9.	Holes
10.10.	Type Ascription
10.11.	Quotation and Antiquotation
10.12.	`do`-Notation
10.13.	Proofs

10.6. Structures and Constructors

Source Code
Report Issues

←10.5. Numeric Literals 10.7. Conditionals→

10.6. Structures and Constructors

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

←10.5. Numeric Literals 10.7. Conditionals→