3.3. Module Structure

3.3.1. Commands and Declarations

3.3.1.1. Definition-Like Commands

The following commands in Lean are definition-like:

  • def

  • abbrev

  • Manual.example

  • theorem

All of these commands cause Lean to elaborate a term based on a signature. With the exception of Manual.example, which discards the result, the resulting expression in Lean's core language is saved for future use in the environment.

syntax
command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers
      definition
syntax
definition ::= ...
    | def `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig := term
      Termination hints are `termination_by` and `decreasing_by`, in that order.

definition ::= ...
    | def `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig
        (| term => term)*
      Termination hints are `termination_by` and `decreasing_by`, in that order.

definition ::= ...
    | def `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig where
        (whereStructField),*
syntax
theorem ::= ...
    | theorem `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` declSig := term
      Termination hints are `termination_by` and `decreasing_by`, in that order.

theorem ::= ...
    | theorem `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` declSig
        (| term => term)*
      Termination hints are `termination_by` and `decreasing_by`, in that order.

theorem ::= ...
    | theorem `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` declSig where
        (whereStructField),*
syntax
abbrev ::= ...
    | abbrev `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig := term
      Termination hints are `termination_by` and `decreasing_by`, in that order.

abbrev ::= ...
    | abbrev `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig
        (| term => term)*
      Termination hints are `termination_by` and `decreasing_by`, in that order.

abbrev ::= ...
    | abbrev `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig where
        (whereStructField),*
syntax
instance ::= ...
    | `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. instance namedPrio `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` : term := term
      Termination hints are `termination_by` and `decreasing_by`, in that order.

instance ::= ...
    | `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. instance namedPrio `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` : term
        (| term => term)*
      Termination hints are `termination_by` and `decreasing_by`, in that order.

instance ::= ...
    | `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. instance namedPrio `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` : term where
        (whereStructField),*
syntax
example ::= ...
    | example `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` (ident  | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole  | bracketedBinder )(ident  | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole  | bracketedBinder ):= term
      Termination hints are `termination_by` and `decreasing_by`, in that order.

example ::= ...
    | example `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` (ident  | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole  | bracketedBinder )(ident
         | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole
         | bracketedBinder
        )(| term => term)*
      Termination hints are `termination_by` and `decreasing_by`, in that order.

example ::= ...
    | example `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` (ident  | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole  | bracketedBinder )(ident  | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole  | bracketedBinder )where
        (whereStructField),*

Opaque constants are defined constants that cannot be reduced to their definition.

syntax
opaque ::= ...
    | opaque `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` declSig
syntax
axiom ::= ...
    | axiom `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` declSig

3.3.1.2. Modifiers

Planned Content

A description of each modifier allowed in the production declModifiers, including documentation comments.

Tracked at issue #52

syntax
declModifiers ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.

A `docComment` node contains a `/--` atom and then the remainder of the comment, `foo -/` in this
example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. docComment
      attributes
      (private
       | protected
      )noncomputable
      unsafe
      (partial
       | nonrec
      )

3.3.1.3. Signatures

Planned Content

Describe signatures, including the following topics:

  • Explicit, implicit, instance-implicit, and strict implicit parameter binders

  • Automatic implicits

  • Argument names and by-name syntax

  • Which parts can be omitted where? Why?

Tracked at issue #53

3.3.1.4. Headers

The header of a definition or declaration specifies the signature of the new constant that is defined.

3.3.2. Section Scopes

Planned Content

Many commands have an effect for the current section scope (sometimes just called "scope" when clear). A section scope ends when a namespace ends, a section ends, or a file ends. They can also be anonymously and locally created via in. Section scopes track the following:

  • The current namespace

  • The open namespaces

  • The values of all options

  • Variable and universe declarations

This section will describe this mechanism.

Tracked at issue #54