1.
What is Lean
2.
Tour of Lean
3.
Setting Up Lean
❱
3.1.
Extended Setup Notes
4.
Theorem Proving in Lean
5.
Functional Programming in Lean
6.
Examples
❱
6.1.
Palindromes
6.2.
Binary Search Trees
6.3.
A Certified Type Checker
6.4.
The Well-Typed Interpreter
6.5.
Dependent de Bruijn Indices
6.6.
Parametric Higher-Order Abstract Syntax
6.7.
Syntax Examples
❱
6.7.1.
Balanced Parentheses
6.7.2.
Arithmetic DSL
Language Manual
7.
The Lean Reference Manual
Other
8.
Frequently Asked Questions
9.
Significant Changes from Lean 3
10.
Syntax Highlighting Lean in LaTeX
11.
User Widgets
12.
Semantic Highlighting
Development
13.
Development Guide
14.
Building Lean
❱
14.1.
Ubuntu Setup
14.2.
macOS Setup
14.3.
Windows MSYS2 Setup
14.4.
Windows with WSL
15.
Bootstrapping
16.
Testing
17.
Debugging
18.
Commit Convention
19.
Release checklist
20.
Building This Manual
21.
Foreign Function Interface
Light (default)
Rust
Coal
Navy
Ayu
Lean Documentation Overview
Examples
Palindromes
Binary Search Trees
A Certified Type Checker
The Well-Typed Interpreter
Dependent de Bruijn Indices
Parametric Higher-Order Abstract Syntax