5. Terms🔗

Planned Content

This chapter will describe Lean's term language, including the following features:

  • Name resolution, including variable occurrences, open declarations and terms

  • fun, with and without pattern matching

  • Literals (some via cross-references to the appropriate types, e.g. String)

Tracked at issue #66

Terms are the principal means of writing mathematics and programs in Lean. The elaborator translates them to Lean's minimal core language, which is then checked by the kernel and compiled for execution. The syntax of terms is arbitrarily extensible; this chapter documents the term syntax that Lean provides out-of-the-box.

  1. 5.1. Identifiers
    1. 5.1.1. Leading .
  2. 5.2. Function Types
  3. 5.3. Functions
    1. 5.3.1. Implicit Parameters
  4. 5.4. Function Application
    1. 5.4.1. Generalized Field Notation
    2. 5.4.2. Pipeline Syntax
  5. 5.5. Literals
    1. 5.5.1. Natural Numbers
    2. 5.5.2. Scientific Numbers
    3. 5.5.3. Strings
    4. 5.5.4. Lists and Arrays
  6. 5.6. Structures and Constructors
  7. 5.7. Conditionals
  8. 5.8. Pattern Matching
    1. 5.8.1. Types
      1. 5.8.1.1. Pattern Equality Proofs
      2. 5.8.1.2. Explicit Motives
      3. 5.8.1.3. Discriminant Refinement
      4. 5.8.1.4. Generalization
    2. 5.8.2. Custom Pattern Functions
    3. 5.8.3. Pattern Matching Functions
    4. 5.8.4. Other Pattern Matching Operators
    5. 5.8.5. Elaborating Pattern Matching
  9. 5.9. Holes
  10. 5.10. Type Ascription
  11. 5.11. Quotation and Antiquotation
  12. 5.12. do-Notation
  13. 5.13. Proofs