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. Examples
    ❱
    1. 5.1. Palindromes
    2. 5.2. Binary Search Trees
    3. 5.3. A Certified Type Checker
    4. 5.4. The Well-Typed Interpreter
    5. 5.5. Dependent de Bruijn Indices
    6. 5.6. Parametric Higher-Order Abstract Syntax
  6. Language Manual
  7. 6. Organizational features
    ❱
    1. 6.1. Sections
    2. 6.2. Namespaces
    3. 6.3. Implicit Arguments
    4. 6.4. Auto Bound Implicit Arguments
  8. 7. Syntax Extensions
    ❱
    1. 7.1. The do Notation
    2. 7.2. String Interpolation
    3. 7.3. User-Defined Notation
    4. 7.4. Macro Overview
    5. 7.5. Elaborators
    6. 7.6. Examples
      ❱
      1. 7.6.1. Balanced Parentheses
      2. 7.6.2. Arithmetic DSL
  9. 8. Declaring New Types
    ❱
    1. 8.1. Enumerated Types
    2. 8.2. Inductive Types
    3. 8.3. Structures
    4. 8.4. Type classes
    5. 8.5. Unification Hints
  10. 9. Builtin Types
    ❱
    1. 9.1. Natural number
    2. 9.2. Integer
    3. 9.3. Fixed precision unsigned integer
    4. 9.4. Float
    5. 9.5. Array
    6. 9.6. List
    7. 9.7. Character
    8. 9.8. String
    9. 9.9. Option
    10. 9.10. Thunk
    11. 9.11. Task and Thread
  11. 10. Functions
  12. Other
  13. 11. Frequently Asked Questions
  14. 12. Significant Changes from Lean 3
  15. 13. Syntax Highlighting Lean in LaTeX
  16. Development
  17. 14. Development Guide
  18. 15. Building Lean
    ❱
    1. 15.1. Ubuntu Setup
    2. 15.2. macOS Setup
    3. 15.3. Windows MSYS2 Setup
    4. 15.4. Windows with WSL
    5. 15.5. Nix Setup (Experimental)
  19. 16. Bootstrapping
  20. 17. Testing
  21. 18. Debugging
  22. 19. Commit Convention
  23. 20. Building This Manual
  24. 21. Foreign Function Interface

Lean Manual

Float