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. 12. Monads
    ❱
    1. 12.1. Functor
    2. 12.2. Applicative
    3. 12.3. Monad
    4. 12.4. Reader
    5. 12.5. State
    6. 12.6. Except
    7. 12.7. Transformers
    8. 12.8. Laws
  14. Other
  15. 13. Frequently Asked Questions
  16. 14. Significant Changes from Lean 3
  17. 15. Syntax Highlighting Lean in LaTeX
  18. 16. User Widgets
  19. 17. Semantic Highlighting
  20. Development
  21. 18. Development Guide
  22. 19. Building Lean
    ❱
    1. 19.1. Ubuntu Setup
    2. 19.2. macOS Setup
    3. 19.3. Windows MSYS2 Setup
    4. 19.4. Windows with WSL
    5. 19.5. Nix Setup (Experimental)
  23. 20. Bootstrapping
  24. 21. Testing
  25. 22. Debugging
  26. 23. Commit Convention
  27. 24. Building This Manual
  28. 25. Foreign Function Interface

Lean Manual

Float