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 `mvcgen` tactic
18.	Functors, Monads and `do`-Notation
19.	Basic Propositions
20.	Basic Types
21.	IO
22.	Dynamic Typing
23.	Iterators
24.	Standard Library
25.	Notations and Macros
26.	Build Tools and Distribution
	Validating a Lean Proof
	Error Explanations
	Release Notes
	Supported Platforms
	Index
	Progress

26. Build Tools and Distribution

26.1.	Lake
26.2.	Managing Toolchains with Elan
26.3.	Reservoir

26.3. Reservoir

Source Code
Report Issues

←26.2. Managing Toolchains with Elan Validating a Lean Proof→

26.3. Reservoir🔗

Planned Content

Concepts
Package and toolchain versions
Tags and builds

Tracked at issue #76

←26.2. Managing Toolchains with Elan Validating a Lean Proof→