Cross-Reference Redirection
Cross-Reference Redirection
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
Source Code
Report Issues
