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 intended for new users. For other documentation, please refer to the Lean documentation site.

This reference manual is not yet complete, but there's enough information to provide value to users. The top priority is to add the missing information as quickly as possible while staying up to date with Lean development. As the rest of the text is written, regular snapshots will be released, tracking upstream changes. This snapshot covers Lean version 4.18.0-nightly-2025-02-16.

Our prioritization of content is based on our best understanding of our users' needs. Please use the issue tracker to help us better understand what you need to know. In particular, please create or upvote issues for topics that are important to you. Your feedback is much appreciated! Once sufficient content is available, we will begin saving snapshots for each release of Lean and making them conveniently available.

API reference documentation is included from the Lean standard library source code. Due to technical limitations at the moment, the Lean terms and examples embedded in it do not render as nicely as we would like. In the near future, we will be working on removing these limitations. Additionally, we will be adding missing API reference documentation and revising and improving the existing API reference documentation.

Release History

2025-02-03

This release updates the contents for Lean version 4.17.0-rc1. It adds descriptions of well-founded recursion, the new partial fixpoint feature, quotient types, and Lake, and the description of structural recursion has been greatly improved. Descriptions and API references for all fixed-width integer types, Int, Fin, Empty, and Option were also added. This release also includes a quick-jump box that can be used to quickly navigate to any documented topic.

2024-12-16

This is the initial release of the reference manual.

  1. 1. Introduction
    1. 1.1. Lean
    2. 1.2. Typographical Conventions
    3. Open-Source Licenses
  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 Type System
    1. 3.1. Functions
    2. 3.2. Propositions
    3. 3.3. Universes
    4. 3.4. Inductive Types
    5. 3.5. Quotients
  4. 4. Interacting with Lean
    1. 4.1. Evaluating Terms
    2. 4.2. Reducing Terms
    3. 4.3. Checking Types
    4. 4.4. Synthesizing Instances
    5. 4.5. Querying the Context
    6. 4.6. Testing Output with #guard_msgs
  5. 5. Source Files
    1. 5.1. Files
    2. 5.2. Module Contents
    3. 5.3. Axioms
    4. 5.4. Attributes
    5. 5.5. Dynamic Typing
    6. 5.6. Coercions
  6. 6. Recursive Definitions
    1. 6.1. Mutual Recursion
    2. 6.2. Structural Recursion
    3. 6.3. Well-Founded Recursion
    4. 6.4. Partial Fixpoint Recursion
    5. 6.5. Partial and Unsafe Recursive Definitions
    6. 6.6. Controlling Reduction
  7. 7. Terms
    1. 7.1. Identifiers
    2. 7.2. Function Types
    3. 7.3. Functions
    4. 7.4. Function Application
    5. 7.5. Literals
    6. 7.6. Structures and Constructors
    7. 7.7. Conditionals
    8. 7.8. Pattern Matching
    9. 7.9. Holes
    10. 7.10. Type Ascription
    11. 7.11. Quotation and Antiquotation
    12. 7.12. do-Notation
    13. 7.13. Proofs
  8. 8. Type Classes
    1. 8.1. Class Declarations
    2. 8.2. Instance Declarations
    3. 8.3. Instance Synthesis
    4. 8.4. Deriving Instances
    5. 8.5. Basic Classes
  9. 9. Functors, Monads and do-Notation
    1. 9.1. Laws
    2. 9.2. Lifting Monads
    3. 9.3. Syntax
    4. 9.4. API Reference
    5. 9.5. Varieties of Monads
  10. 10. IO
    1. 10.1. Logical Model
    2. 10.2. Control Structures
    3. 10.3. Console Output
    4. 10.4. Mutable References
    5. 10.5. Files, File Handles, and Streams
    6. 10.6. Environment Variables
    7. 10.7. Timing
    8. 10.8. Processes
    9. 10.9. Random Numbers
    10. 10.10. Tasks and Threads
  11. 11. Tactic Proofs
    1. 11.1. Running Tactics
    2. 11.2. Reading Proof States
    3. 11.3. The Tactic Language
    4. 11.4. Options
    5. 11.5. Tactic Reference
    6. 11.6. Targeted Rewriting with conv
    7. 11.7. Naming Bound Variables
    8. 11.8. Custom Tactics
  12. 12. The Simplifier
    1. 12.1. Invoking the Simplifier
    2. 12.2. Rewrite Rules
    3. 12.3. Simp sets
    4. 12.4. Simp Normal Forms
    5. 12.5. Terminal vs Non-Terminal Positions
    6. 12.6. Configuring Simplification
    7. 12.7. Simplification vs Rewriting
  13. 13. Basic Propositions
    1. 13.1. Truth
    2. 13.2. Logical Connectives
    3. 13.3. Quantifiers
    4. 13.4. Propositional Equality
  14. 14. Basic Types
    1. 14.1. Natural Numbers
    2. 14.2. Integers
    3. 14.3. Finite Natural Numbers
    4. 14.4. Fixed-Precision Integer Types
    5. 14.5. Bitvectors
    6. 14.6. Floating-Point Numbers
    7. 14.7. Characters
    8. 14.8. Strings
    9. 14.9. The Unit Type
    10. 14.10. The Empty Type
    11. 14.11. Booleans
    12. 14.12. Optional Values
    13. 14.13. Tuples
    14. 14.14. Sum Types
    15. 14.15. Linked Lists
    16. 14.16. Arrays
    17. 14.17. Subtypes
    18. 14.18. Lazy Computations
    19. 14.19. Tasks and Threads
  15. 15. Standard Library
  16. 16. Notations and Macros
    1. 16.1. Custom Operators
    2. 16.2. Precedence
    3. 16.3. Notations
    4. 16.4. Defining New Syntax
    5. 16.5. Macros
    6. 16.6. Elaborators
  17. 17. Output from Lean
  18. 18. Elan
  19. 19. Build Tools and Distribution
    1. 19.1. Lake
    2. 19.2. Reservoir
  20. Index