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
    2. 3.6.2. Instance Declarations
    3. 3.6.3. Instance Synthesis
    4. 3.6.4. Deriving Instances
      1. 3.6.4.1. Deriving Handlers