3. The Lean Language

  1. 3.1. Files
    1. 3.1.1. Modules
      1. 3.1.1.1. Encoding and Representation
      2. 3.1.1.2. Concrete Syntax
        1. 3.1.1.2.1. Whitespace
        2. 3.1.1.2.2. Comments
        3. 3.1.1.2.3. Keywords and Identifiers
      3. 3.1.1.3. Structure
        1. 3.1.1.3.1. Module Headers
        2. 3.1.1.3.2. Commands
      4. 3.1.1.4. Contents
    2. 3.1.2. Packages, Libraries, and Targets
  2. 3.2. The Type System
    1. 3.2.1. Functions
      1. 3.2.1.1. Functions
      2. 3.2.1.2. Currying
      3. 3.2.1.3. Implicit Functions
      4. 3.2.1.4. Pattern Matching
      5. 3.2.1.5. Extensionality
      6. 3.2.1.6. Totality and Termination
    2. 3.2.2. Propositions
    3. 3.2.3. Universes
      1. 3.2.3.1. Predicativity
      2. 3.2.3.2. Polymorphism
        1. 3.2.3.2.1. Level Expressions
        2. 3.2.3.2.2. Universe Variable Bindings
        3. 3.2.3.2.3. Universe Unification
    4. 3.2.4. Inductive Types
      1. 3.2.4.1. Inductive Type Declarations
        1. 3.2.4.1.1. Parameters and Indices
        2. 3.2.4.1.2. Example Inductive Types
        3. 3.2.4.1.3. Anonymous Constructor Syntax
        4. 3.2.4.1.4. Deriving Instances
      2. 3.2.4.2. Structure Declarations
        1. 3.2.4.2.1. Structure Parameters
        2. 3.2.4.2.2. Fields
        3. 3.2.4.2.3. Structure Constructors
        4. 3.2.4.2.4. Structure Inheritance
      3. 3.2.4.3. Logical Model
        1. 3.2.4.3.1. Recursors
          1. 3.2.4.3.1.1. Recursor Types
            1. 3.2.4.3.1.1.1. Subsingleton Elimination
          2. 3.2.4.3.1.2. Reduction
        2. 3.2.4.3.2. Well-Formedness Requirements
          1. 3.2.4.3.2.1. Universe Levels
          2. 3.2.4.3.2.2. Strict Positivity
          3. 3.2.4.3.2.3. Prop vs Type
        3. 3.2.4.3.3. Constructions for Termination Checking
      4. 3.2.4.4. Run-Time Representation
        1. 3.2.4.4.1. Exceptions
        2. 3.2.4.4.2. Relevance
        3. 3.2.4.4.3. Trivial Wrappers
        4. 3.2.4.4.4. Other Inductive Types
          1. 3.2.4.4.4.1. FFI
      5. 3.2.4.5. Mutual Inductive Types
        1. 3.2.4.5.1. Requirements
          1. 3.2.4.5.1.1. Mutual Dependencies
          2. 3.2.4.5.1.2. Parameters Must Match
          3. 3.2.4.5.1.3. Universe Levels
          4. 3.2.4.5.1.4. Positivity
        2. 3.2.4.5.2. Recursors
        3. 3.2.4.5.3. Run-Time Representation
    5. 3.2.5. Quotients
  3. 3.3. Module Contents
    1. 3.3.1. Commands and Declarations
      1. 3.3.1.1. Definition-Like Commands
      2. 3.3.1.2. Modifiers
      3. 3.3.1.3. Signatures
      4. 3.3.1.4. Headers
    2. 3.3.2. Section Scopes
  4. 3.4. Axioms
  5. 3.5. Recursive Definitions
    1. 3.5.1. Structural Recursion
      1. 3.5.1.1. Mutual Structural Recursion
    2. 3.5.2. Well-Founded Recursion
    3. 3.5.3. Controlling Reduction
    4. 3.5.4. Partial and Unsafe Recursive Definitions
  6. 3.6. Type Classes
    1. 3.6.1. Class Declarations
      1. 3.6.1.1. Sum Types as Classes
      2. 3.6.1.2. Class Abbreviations
    2. 3.6.2. Instance Declarations
      1. 3.6.2.1. Recursive Instances
      2. 3.6.2.2. Instances of class inductives
      3. 3.6.2.3. Instance Priorities
      4. 3.6.2.4. Default Instances
      5. 3.6.2.5. The Instance Attribute
    3. 3.6.3. Instance Synthesis
      1. 3.6.3.1. Instance Search Summary
      2. 3.6.3.2. Instance Search Problems
      3. 3.6.3.3. Candidate Instances
      4. 3.6.3.4. Instance Parameters and Synthesis
      5. 3.6.3.5. Output Parameters
      6. 3.6.3.6. Default Instances
      7. 3.6.3.7. “Morally Canonical” Instances
      8. 3.6.3.8. Options
    4. 3.6.4. Deriving Instances
      1. 3.6.4.1. Deriving Handlers
    5. 3.6.5. Basic Classes
      1. 3.6.5.1. Boolean Equality Tests
      2. 3.6.5.2. Ordering
      3. 3.6.5.3. Decidability
      4. 3.6.5.4. Inhabited Types
      5. 3.6.5.5. Visible Representations
      6. 3.6.5.6. Arithmetic and Bitwise Operators
      7. 3.6.5.7. Append
      8. 3.6.5.8. Data Lookups
  7. 3.7. Dynamic Typing