The Lean Language Reference

  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. Types
    3. 3.3. Module Structure
    4. 3.4. Axioms
    5. 3.5. Recursive Definitions
    6. 3.6. Type Classes
  4. 4. Terms
  5. 5. Monads and do-Notation
  6. 6. IO
  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. Floating-Point Numbers
    5. 9.5. Characters
    6. 9.6. Strings
    7. 9.7. Linked Lists
    8. 9.8. Arrays
    9. 9.9. Lazy Computations
    10. 9.10. Tasks and Threads
  10. 10. Standard Library
    1. 10.1. Optional Values
  11. 11. Notations and Macros
    1. 11.1. Notations
    2. 11.2. Syntax Categories and Extensions
    3. 11.3. Macros
    4. 11.4. Elaborators
  12. 12. Elan
  13. 13. Lake and Reservoir
    1. 13.1. Lake
    2. 13.2. Reservoir
  14. Index