The Lean Language Reference🔗

This is the Lean Language Reference, an in-progress reference work on Lean. It is intended to be a comprehensive, precise description of Lean: a reference work in which Lean users can look up detailed information, rather than a tutorial for new users. For other documentation, please refer to the Lean documentation site.

  1. 1. Introduction
    1. 1.1. Lean
    2. 1.2. Typographical Conventions
  2. 2. Elaboration and Compilation
    1. 2.1. Parsing
    2. 2.2. Macro Expansion and Elaboration
    3. 2.3. The Kernel
    4. 2.4. Elaboration Results
    5. 2.5. Initialization
  3. 3. The Lean Language
    1. 3.1. Files
    2. 3.2. The Type System
    3. 3.3. Module Contents
    4. 3.4. Axioms
    5. 3.5. Recursive Definitions
    6. 3.6. Attributes
    7. 3.7. Type Classes
    8. 3.8. Dynamic Typing
    9. 3.9. Coercions
  4. 4. Terms
  5. 5. Monads and do-Notation
  6. 6. IO
    1. 6.1. Logical Model
    2. 6.2. Control Structures
    3. 6.3. Console Output
    4. 6.4. Mutable References
    5. 6.5. Files, File Handles, and Streams
    6. 6.6. Environment Variables
    7. 6.7. Timing
    8. 6.8. Processes
    9. 6.9. Random Numbers
    10. 6.10. Tasks and Threads
  7. 7. Tactic Proofs
    1. 7.1. Running Tactics
    2. 7.2. Reading Proof States
    3. 7.3. The Tactic Language
    4. 7.4. Options
    5. 7.5. Tactic Reference
    6. 7.6. Targeted Rewriting with conv
    7. 7.7. Custom Tactics
  8. 8. The Simplifier
    1. 8.1. Invoking the Simplifier
    2. 8.2. Rewrite Rules
    3. 8.3. Simp sets
    4. 8.4. Simp Normal Forms
    5. 8.5. Terminal vs Non-Terminal Positions
    6. 8.6. Configuring Simplification
    7. 8.7. Simplification vs Rewriting
  9. 9. Basic Types
    1. 9.1. Natural Numbers
    2. 9.2. Integers
    3. 9.3. Fixed-Precision Integer Types
    4. 9.4. Bitvectors
    5. 9.5. Floating-Point Numbers
    6. 9.6. Characters
    7. 9.7. Strings
    8. 9.8. The Unit Type
    9. 9.9. Booleans
    10. 9.10. Linked Lists
    11. 9.11. Arrays
    12. 9.12. Lazy Computations
    13. 9.13. Tasks and Threads
  10. 10. Standard Library
    1. 10.1. Optional Values
  11. 11. Notations and Macros
    1. 11.1. Custom Operators
    2. 11.2. Precedence
    3. 11.3. Notations
    4. 11.4. Defining New Syntax
    5. 11.5. Macros
    6. 11.6. Elaborators
  12. 12. Output from Lean
  13. 13. Elan
  14. 14. Lake and Reservoir
    1. 14.1. Lake
    2. 14.2. Reservoir
  15. Index