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

Lean Manual

Examples

  • Palindromes
  • Binary Search Trees
  • A Certified Type Checker
  • The Well-Typed Interpreter
  • Dependent de Bruijn Indices
  • Parametric Higher-Order Abstract Syntax