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

The Lean Reference Manual

  • 1. Using Lean
  • 2. Lexical Structure
  • 3. Expressions
  • 4. Declarations
  • 5. Other Commands
  • 6. Tactics
  • 7. Programming
  • 8. Metaprogramming
  • 9. Libraries

  • PDF version
  • Lean Home

Quick search

©2017, Jeremy Avigad, Gabriel Ebner, Sebastian Ullrich. | Powered by Sphinx 1.6.3 & Alabaster 0.7.10 | Page source