3.3. Module Contents

As described in the section on the syntax of files, a Lean module consists of a header followed by a sequence of commands.

3.3.1. Commands and Declarations

After the header, every top-level phrase of a Lean module is a command. Commands may add new types, define new constants, or query Lean for information. Commands may even change the syntax used to parse subsequent commands.

Planned Content

  • Describe the various families of available commands (definition-like, #eval-like, etc).

  • Refer to specific chapters that describe major commands, such as inductive.

Tracked at issue #100

3.3.1.1. Definition-Like Commands

Planned Content

  • Precise descriptions of these commands and their syntax

  • Comparison of each kind of definition-like command to the others

Tracked at issue #101

The following commands in Lean are definition-like: Render commands as their name (a la tactic index)

All of these commands cause Lean to elaborate a term based on a signature. With the exception of example, which discards the result, the resulting expression in Lean's core language is saved for future use in the environment. The Lean.Parser.Command.declaration : commandinstance command is described in the section on instance declarations.

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 := termTermination 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 := termTermination 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 := termTermination 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
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 ):= termTermination 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 implicit parameters

  • 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

syntax

Globally-scoped declarations (the default) are in effect whenever the module in which they're established is transitively imported. They are indicated by the absence of another scope modifier.

attrKind ::=
    `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`.

Locally-scoped declarations are in effect only for the extent of the section scope in which they are established.

attrKind ::= ...
    | `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. local

Scoped declarations are in effect whenever the namespace in which they are established is opened.

attrKind ::= ...
    | `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. scoped