Summary

• What is Lean
• Tour of Lean
• Setting Up Lean
  • Extended Setup Notes
• Theorem Proving in Lean
• Functional Programming in Lean
• Examples
  • Palindromes
  • Binary Search Trees
  • A Certified Type Checker
  • The Well-Typed Interpreter
  • Dependent de Bruijn Indices
  • Parametric Higher-Order Abstract Syntax
  • Syntax Examples
    • Balanced Parentheses
    • Arithmetic DSL

Language Manual

• The Lean Reference Manual

Other

• Frequently Asked Questions
• Significant Changes from Lean 3
• Syntax Highlighting Lean in LaTeX
• User Widgets
• Semantic Highlighting

Development

• Development Guide
• Building Lean
  • Ubuntu Setup
  • macOS Setup
  • Windows MSYS2 Setup
  • Windows with WSL
• Bootstrapping
• Testing
• Debugging
• Commit Convention
• Release checklist
• Building This Manual
• Foreign Function Interface