1.
What is Lean
2.
Tour of Lean
3.
Setting Up Lean
❱
3.1.
Extended Setup Notes
4.
Theorem Proving in Lean
5.
Examples
❱
5.1.
Palindromes
5.2.
Binary Search Trees
5.3.
A Certified Type Checker
5.4.
The Well-Typed Interpreter
5.5.
Dependent de Bruijn Indices
5.6.
Parametric Higher-Order Abstract Syntax
Language Manual
6.
Organizational features
❱
6.1.
Sections
6.2.
Namespaces
6.3.
Implicit Arguments
6.4.
Auto Bound Implicit Arguments
7.
Syntax Extensions
❱
7.1.
The do Notation
7.2.
String Interpolation
7.3.
User-Defined Notation
7.4.
Macro Overview
7.5.
Elaborators
7.6.
Examples
❱
7.6.1.
Balanced Parentheses
7.6.2.
Arithmetic DSL
8.
Declaring New Types
❱
8.1.
Enumerated Types
8.2.
Inductive Types
8.3.
Structures
8.4.
Type classes
8.5.
Unification Hints
9.
Builtin Types
❱
9.1.
Natural number
9.2.
Integer
9.3.
Fixed precision unsigned integer
9.4.
Float
9.5.
Array
9.6.
List
9.7.
Character
9.8.
String
9.9.
Option
9.10.
Thunk
9.11.
Task and Thread
10.
Functions
Other
11.
Frequently Asked Questions
12.
Significant Changes from Lean 3
13.
Syntax Highlighting Lean in LaTeX
Development
14.
Development Guide
15.
Building Lean
❱
15.1.
Ubuntu Setup
15.2.
macOS Setup
15.3.
Windows MSYS2 Setup
15.4.
Windows with WSL
15.5.
Nix Setup (Experimental)
16.
Bootstrapping
17.
Testing
18.
Debugging
19.
Commit Convention
20.
Building This Manual
21.
Foreign Function Interface
Light (default)
Rust
Coal
Navy
Ayu
Lean Manual
Float