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: 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.
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`
Move instance
to type classes section with a backreference from here
instance ::= ... |instance namedPrio
`attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`.
: 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.
instance ::= ... |instance namedPrio
`attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`.
: term (| 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.
instance ::= ... |instance namedPrio
`attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`.
: term where (whereStructField),*
`declSig` matches the signature of a declaration with required type: a list of binders and then `: 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.
-
Precision and examples; list all of them here
-
Mention interaction with autoimplicits
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