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
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.
-
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
-
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:
-
def
-
abbrev
-
theorem
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 : command
instance
command is described in the section on instance declarations.
definition ::= ... | defdeclId
`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names
optDeclSig := term
`optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`
Termination hints are `termination_by` and `decreasing_by`, in that order.
definition ::= ... | defdeclId
`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names
optDeclSig (| term => term)*
`optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`
Termination hints are `termination_by` and `decreasing_by`, in that order.
definition ::= ... | defdeclId
`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names
optDeclSig where (whereStructField),*
`optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`
theorem ::= ... | theoremdeclId
`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names
declSig := term
`declSig` matches the signature of a declaration with required type: a list of binders and then `: type`
Termination hints are `termination_by` and `decreasing_by`, in that order.
theorem ::= ... | theoremdeclId
`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names
declSig (| term => term)*
`declSig` matches the signature of a declaration with required type: a list of binders and then `: type`
Termination hints are `termination_by` and `decreasing_by`, in that order.
theorem ::= ... | theoremdeclId
`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names
declSig where (whereStructField),*
`declSig` matches the signature of a declaration with required type: a list of binders and then `: type`
abbrev ::= ... | abbrevdeclId
`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names
optDeclSig := term
`optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`
Termination hints are `termination_by` and `decreasing_by`, in that order.
abbrev ::= ... | abbrevdeclId
`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names
optDeclSig (| term => term)*
`optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`
Termination hints are `termination_by` and `decreasing_by`, in that order.
abbrev ::= ... | abbrevdeclId
`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names
optDeclSig where (whereStructField),*
`optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`
example ::= ... | example(ident |
`optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`
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
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).
Termination hints are `termination_by` and `decreasing_by`, in that order.
example ::= ... | example(ident |
`optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`
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)*
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).
Termination hints are `termination_by` and `decreasing_by`, in that order.
example ::= ... | example(ident |
`optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`
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),*
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).
Opaque constants are defined constants that cannot be reduced to their definition.
opaque ::= ... | opaquedeclId
`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names
declSig
`declSig` matches the signature of a declaration with required type: a list of binders and then `: type`
axiom ::= ... | axiomdeclId
`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names
declSig
`declSig` matches the signature of a declaration with required type: a list of binders and then `: type`
3.3.1.2. Modifiers
A description of each modifier allowed in the production declModifiers
, including documentation comments.
Tracked at issue #52
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.
docComment attributes (private | protected )noncomputable unsafe (partial | nonrec )
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.
3.3.1.3. Signatures
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
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