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
Language Manual
7.
Organizational features
❱
7.1.
Sections
7.2.
Namespaces
7.3.
Implicit Arguments
7.4.
Auto Bound Implicit Arguments
8.
Syntax Extensions
❱
8.1.
The do Notation
8.2.
String Interpolation
8.3.
User-Defined Notation
8.4.
Macro Overview
8.5.
Elaborators
8.6.
Examples
❱
8.6.1.
Balanced Parentheses
8.6.2.
Arithmetic DSL
9.
Declaring New Types
❱
9.1.
Enumerated Types
9.2.
Inductive Types
9.3.
Structures
9.4.
Type classes
9.5.
Unification Hints
10.
Builtin Types
❱
10.1.
Natural number
10.2.
Integer
10.3.
Fixed precision unsigned integer
10.4.
Float
10.5.
Array
10.6.
List
10.7.
Character
10.8.
String
10.9.
Option
10.10.
Thunk
10.11.
Task and Thread
11.
Functions
Other
12.
Frequently Asked Questions
13.
Significant Changes from Lean 3
14.
Syntax Highlighting Lean in LaTeX
Development
15.
Development Guide
16.
Building Lean
❱
16.1.
Ubuntu Setup
16.2.
macOS Setup
16.3.
Windows MSYS2 Setup
16.4.
Windows with WSL
16.5.
Nix Setup (Experimental)
17.
Bootstrapping
18.
Testing
19.
Debugging
20.
Commit Convention
21.
Building This Manual
22.
Foreign Function Interface
Light (default)
Rust
Coal
Navy
Ayu
Lean Manual
Examples
Palindromes
Binary Search Trees
A Certified Type Checker
The Well-Typed Interpreter
Dependent de Bruijn Indices
Parametric Higher-Order Abstract Syntax