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: Render commands as their name (a la tactic index)

  • 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),*

Move instance to type classes section with a backreference from here

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.

  • Precision and examples; list all of them here

  • Mention interaction with autoimplicits

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