←
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 Propositions
14.
Basic Types
15.
Standard Library
16.
Notations and Macros
17.
Output from Lean
18.
Elan
19.
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.