The Lean Reference Manual

• 1. Using Lean
  • 1.1. Using Lean Online
  • 1.2. Using Lean with VSCode
  • 1.3. Using Lean with Emacs
  • 1.4. Using the Package Manager
• 2. Lexical Structure
  • 2.1. Symbols and Commands
  • 2.2. Identifiers
  • 2.3. String Literals
  • 2.4. Char Literals
  • 2.5. Numeric Literals
  • 2.6. Quoted Symbols
  • 2.7. Doc Comments
  • 2.8. Field Notation
• 3. Expressions
  • 3.1. Universes
  • 3.2. Expression Syntax
  • 3.3. Implicit Arguments
  • 3.4. Basic Data Types and Assertions
  • 3.5. Constructors, Projections, and Matching
  • 3.6. Structured Proofs
  • 3.7. Computation
  • 3.8. Axioms
• 4. Declarations
  • 4.1. Declaration Names
  • 4.2. Contexts and Telescopes
  • 4.3. Basic Declarations
  • 4.4. Inductive Types
  • 4.5. Inductive Families
  • 4.6. Mutual and Nested Inductive Definitions
  • 4.7. The Equation Compiler
  • 4.8. Match Expressions
  • 4.9. Structures and Records
  • 4.10. Type Classes
• 5. Other Commands
  • 5.1. Universes and Variables
  • 5.2. Sections
  • 5.3. Namespaces
  • 5.4. Attributes
  • 5.5. Options
  • 5.6. Instructions
  • 5.7. Notation Declarations
• 6. Tactics
  • 6.1. Tactic Mode
  • 6.2. Basic Tactics
  • 6.3. Equality and Other Relations
  • 6.4. Structured Tactic Proofs
  • 6.5. Inductive Types
  • 6.6. Tactic Combinators
  • 6.7. The Rewriter
  • 6.8. The Simplifier and Congruence Closure
  • 6.9. Other Tactics
  • 6.10. Conversions
  • 6.11. The SMT State
• 7. Programming
  • 7.1. The Virtual Machine
  • 7.2. Monads
• 8. Metaprogramming
  • 8.1. Quotations
  • 8.2. User Defined Attributes
• 9. Libraries
  • 9.1. The Standard Library
  • 9.2. The Mathematics Library
  • 9.3. Other Libraries
  • 9.4. User-Maintained Libraries