3.3. モジュールの内容（Module Contents）

ファイルの構文に関する節 で説明したように、Lean のモジュールはヘッダとそれに続く一連のコマンドで構成されます。

3.3.1. コマンドと宣言（Commands and Declaration）

ヘッダの後にある、Lean モジュールのトップレベルのフレーズはすべてコマンドです。コマンドは新しい型を追加したり、新しい定数を定義したり、Lean に情報を問い合わせたりします。コマンドは 後続のコマンドをパースするために使用される構文を変更する ことさえもできます。

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

以下の Lean のコマンドは定義に類するものです：

これらのコマンドはすべて Lean によってシグネチャに応じた項へ エラボレート されます。結果を破棄する example を除き、Lean のコア言語での結果の式は将来の環境で使用するために保存されます。 Lean.Parser.Command.declaration : commandinstance コマンドについては インスタンス宣言の節 で記述します。

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*

不透明な定数 はそれらの定義へ簡約されない定数を定義します。

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）

定義または宣言の ヘッダ （header）は定義される新しい定数のシグネチャを指定します。

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