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.
Iterators
22.
Notations and Macros
23.
Run-Time Code
24.
Build Tools and Distribution
Validating a Lean Proof
Error Explanations
Release Notes
Supported Platforms
Index
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.11.
Quotation and Antiquotation
Source Code
Report Issues
←
10.10. Type Ascription
10.12. do-Notation
→
10.11. Quotation and Antiquotation
🔗
Quotation terms are described in the
section on quotation
.
←
10.10. Type Ascription
10.12. do-Notation
→
