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
vcgen
tactic
18.
The
mvcgen
tactic
19.
Functors, Monads and
do
-Notation
20.
Basic Propositions
21.
Basic Types
22.
IO
23.
Iterators
24.
Notations and Macros
25.
Build Tools and Distribution
26.
Linters and Code Quality
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.11.
Quotation and Antiquotation
Source Code
Report Issues
←
13.10. Type Ascription
13.12. do-Notation
→
13.11. Quotation and Antiquotation
🔗
Quotation terms are described in the
section on quotation
.
←
13.10. Type Ascription
13.12. do-Notation
→
