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
12.
Monads
❱
12.1.
Functor
12.2.
Applicative
12.3.
Monad
12.4.
Reader
12.5.
State
12.6.
Except
12.7.
Transformers
12.8.
Laws
Other
13.
Frequently Asked Questions
14.
Significant Changes from Lean 3
15.
Syntax Highlighting Lean in LaTeX
16.
User Widgets
17.
Semantic Highlighting
Development
18.
Development Guide
19.
Building Lean
❱
19.1.
Ubuntu Setup
19.2.
macOS Setup
19.3.
Windows MSYS2 Setup
19.4.
Windows with WSL
20.
Bootstrapping
21.
Testing
22.
Debugging
23.
Commit Convention
24.
Release checklist
25.
Building This Manual
26.
Foreign Function Interface
Light (default)
Rust
Coal
Navy
Ayu
Lean Manual
Inductive Types
Theorem Proving in Lean
has a chapter about inductive datatypes.