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.	Dynamic Typing
24.	Iterators
25.	Standard Library
26.	Notations and Macros
27.	Build Tools and Distribution
28.	Linters and Code Quality
29.	External Kernels
	Validating a Lean Proof
	Error Explanations
	Release Notes
	Supported Platforms
	Index
	Progress

27. Build Tools and Distribution

27.1.	Lake
27.2.	Managing Toolchains with Elan
27.3.	Reservoir

27.3. Reservoir

Source Code
Report Issues

←27.2. Managing Toolchains with Elan 28. Linters and Code Quality→

27.3. Reservoir🔗

Planned Content

Concepts
Package and toolchain versions
Tags and builds

Tracked at issue #76

←27.2. Managing Toolchains with Elan 28. Linters and Code Quality→