Cross-Reference Redirection

Table of Contents

1.	Preface
2.	Basics: Functional Programming in Lean
3.	Induction: Proof by Induction
4.	UsingLean: Using the Full Power of a Proof Assistant
5.	Lists: Working with Structured Data
6.	Poly: Polymorphism and Higher-Order Functions
7.	Tactics: More Basic Tactics
8.	Logic in Lean
9.	IndProp: Inductively Defined Propositions
10.	Automation: More Automation
11.	Typeclasses
12.	Postscript

Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC