6. 命名空间和部分🔗

名称被组织成分层的 namespaces，它们是名称的集合。命名空间是 Lean 中组织 API 的主要方式：它们提供操作本体，对相关项进行分组。此外，虽然这不是通过在命名空间中给它们命名来完成的，但语法扩展、实例和属性等功能的效果可以附加到命名空间。

将操作排序到名称空间中可以从全局角度从概念上组织库。然而，任何给定的 Lean 文件通常不会同等地使用所有名称。 Sections 提供了一种对全局可用名称集合的本地视图进行排序的方法，以及精确控制编译器选项以及语言扩展、实例和属性的范围的方法。它们还允许使用 Lean.Parser.Command.variable : commandDeclares one or more typed variables, or modifies whether already-declared variables are implicit. Introduces variables that can be used in definitions within the same `namespace` or `section` block. When a definition mentions a variable, Lean will add it as an argument of the definition. This is useful in particular when writing many definitions that have parameters in common (see below for an example). Variable declarations have the same flexibility as regular function parameters. In particular they can be [explicit, implicit][binder docs], or [instance implicit][tpil classes] (in which case they can be anonymous). This can be changed, for instance one can turn explicit variable `x` into an implicit one with `variable {x}`. Note that currently, you should avoid changing how variables are bound and declare new variables at the same time; see [issue 2789] for more on this topic. In *theorem bodies* (i.e. proofs), variables are not included based on usage in order to ensure that changes to the proof cannot change the statement of the overall theorem. Instead, variables are only available to the proof if they have been mentioned in the theorem header or in an `include` command or are instance implicit and depend only on such variables. See [*Variables and Sections* from Theorem Proving in Lean][tpil vars] for a more detailed discussion. [tpil vars]: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#variables-and-sections (Variables and Sections on Theorem Proving in Lean) [tpil classes]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html (Type classes on Theorem Proving in Lean) [binder docs]: https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.BinderInfo (Documentation for the BinderInfo type) [issue 2789]: https://github.com/leanprover/lean4/issues/2789 (Issue 2789 on github) ## Examples ```lean section variable {α : Type u} -- implicit (a : α) -- explicit [instBEq : BEq α] -- instance implicit, named [Hashable α] -- instance implicit, anonymous def isEqual (b : α) : Bool := a == b #check isEqual -- isEqual.{u} {α : Type u} (a : α) [instBEq : BEq α] (b : α) : Bool variable {a} -- `a` is implicit now def eqComm {b : α} := a == b ↔ b == a #check eqComm -- eqComm.{u} {α : Type u} {a : α} [instBEq : BEq α] {b : α} : Prop end ``` The following shows a typical use of `variable` to factor out definition arguments: ```lean variable (Src : Type) structure Logger where trace : List (Src × String) #check Logger -- Logger (Src : Type) : Type namespace Logger -- switch `Src : Type` to be implicit until the `end Logger` variable {Src} def empty : Logger Src where trace := [] #check empty -- Logger.empty {Src : Type} : Logger Src variable (log : Logger Src) def len := log.trace.length #check len -- Logger.len {Src : Type} (log : Logger Src) : Nat variable (src : Src) [BEq Src] -- at this point all of `log`, `src`, `Src` and the `BEq` instance can all become arguments def filterSrc := log.trace.filterMap fun (src', str') => if src' == src then some str' else none #check filterSrc -- Logger.filterSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : List String def lenSrc := log.filterSrc src |>.length #check lenSrc -- Logger.lenSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : Nat end Logger ``` The following example demonstrates availability of variables in proofs: ```lean variable {α : Type} -- available in the proof as indirectly mentioned through `a` [ToString α] -- available in the proof as `α` is included (a : α) -- available in the proof as mentioned in the header {β : Type} -- not available in the proof [ToString β] -- not available in the proof theorem ex : a = a := rfl ``` After elaboration of the proof, the following warning will be generated to highlight the unused hypothesis: ``` included section variable '[ToString α]' is not used in 'ex', consider excluding it ``` In such cases, the offending variable declaration should be moved down or into a section so that only theorems that do depend on it follow it until the end of the section.variable 命令集中声明并根据需要传播许多声明共享的参数。

6.1. 命名空间🔗

包含句点的名称（不在 guillemets 内）是分层名称；句点分隔名称的组成部分。名称中除了最后一个组成部分之外的所有组成部分都是名称空间，而最后一个组成部分是名称本身。

命名空间用于对相关定义、定理、类型和其他声明进行分组。当命名空间对应于类型的名称时，可以使用通用字段表示法来访问其内容。除了组织名称之外，命名空间还对语法扩展、属性和实例进行分组。

命名空间与 modules 正交：模块是一起详细说明、编译和加载的代码单元，但模块名称与其提供的名称之间没有必然联系。模块可以包含任何名称空间中的名称，并且分层模块的嵌套结构与分层名称空间的嵌套结构无关。

有一个根命名空间，通常通过简单地省略命名空间来表示。可以通过以 _root_ 开头的名称来明确指示。在名称将相对于环境命名空间（例如来自节范围）或本地范围进行解释的上下文中，这可能是必要的。

Explicit Root Namespace

当前命名空间中的名称优先于根命名空间中的名称。在此示例中，Forest.statement 定义中的 color 引用 Forest.color：

def color := "yellow"
namespace Forest
def color := "green"
def statement := s!"Lemons are {color}"
end Forest

"Lemons are green"#eval Forest.statement

"Lemons are green"

在 Forest 命名空间内，对根命名空间中的 color 的引用必须使用 _root_ 进行限定：

namespace Forest
def nextStatement :=
  s!"Ripe lemons are {_root_.color}, not {color}"
end Forest

"Ripe lemons are yellow, not green"#eval Forest.nextStatement

"Ripe lemons are yellow, not green"

Live ↪

6.1.1. 命名空间和节范围🔗

每个节范围都有一个当前命名空间，它由 Lean.Parser.Command.namespace : command`namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside the section: * Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the full name `Nat.seventeen`. * Names introduced by `export` declarations are also prefixed by the identifier. * All names starting with `<id>.` become available in the namespace without the prefix. These names are preferred over names introduced by outer namespaces or `open`. * Within a namespace, declarations can be `protected`, which excludes them from the effects of opening the namespace. As with `section`, namespaces can be nested and the scope of a namespace is terminated by a corresponding `end <id>` or the end of the file. `namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.namespace 命令确定。Lean.Parser.Command.namespace : command`namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside the section: * Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the full name `Nat.seventeen`. * Names introduced by `export` declarations are also prefixed by the identifier. * All names starting with `<id>.` become available in the namespace without the prefix. These names are preferred over names introduced by outer namespaces or `open`. * Within a namespace, declarations can be `protected`, which excludes them from the effects of opening the namespace. As with `section`, namespaces can be nested and the scope of a namespace is terminated by a corresponding `end <id>` or the end of the file. `namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.namespace 命令在有关引入节范围的命令的部分中进行了描述。在节范围内声明的名称将添加到当前命名空间。如果声明的名称有多个组件，则其命名空间嵌套在当前命名空间内；声明的当前命名空间的主体是嵌套命名空间。节范围还包括一组 opened 命名空间，这些命名空间的内容在没有附加限定的范围内。解析特定名称的标识符会考虑当前命名空间和打开的命名空间。但是，protected 声明（即具有 protected modifier 的声明）在打开其命名空间时不会进入作用域。关于标识符作为术语的部分中描述了将标识符解析为考虑当前命名空间和打开的命名空间的名称的规则。

Current Namespace

定义归纳类型会导致该类型的构造函数被放置在其命名空间中，在本例中为 HotDrink.coffee、HotDrink.tea 和 HotDrink.cocoa。

inductive HotDrink where
  | coffee
  | tea
  | cocoa

在命名空间之外，除非打开命名空间，否则必须限定这些名称：

HotDrink.tea : HotDrink#check HotDrink.tea

HotDrink.tea : HotDrink

#check Unknown identifier `tea`tea

Unknown identifier `tea`

section
open HotDrink
HotDrink.tea : HotDrink#check tea
end

HotDrink.tea : HotDrink

如果直接在 HotDrink 命名空间内定义函数，则将使用设置为 HotDrink 的当前命名空间来详细说明函数的主体。构造函数的范围是：

def HotDrink.ofString? : String → Option HotDrink
  | "coffee" => some coffee
  | "tea" => some tea
  | "cocoa" => some cocoa
  | _ => none

定义另一个归纳类型会创建一个新的命名空间：

inductive ColdDrink where
  | water
  | juice

在 HotDrink 命名空间内，可以在没有显式前缀的情况下定义 HotDrink.toString。在 ColdDrink 命名空间中定义函数需要显式 _root_ 限定符以避免定义 HotDrink.ColdDrink.toString：

namespace HotDrink

def toString : HotDrink → String
  | coffee => "coffee"
  | tea => "tea"
  | cocoa => "cocoa"

def _root_.ColdDrink.toString : ColdDrink → String
  | .water => "water"
  | .juice => "juice"

end HotDrink

Live ↪

Lean.Parser.Command.open : commandMakes names from other namespaces visible without writing the namespace prefix. Names that are made available with `open` are visible within the current `section` or `namespace` block. This makes referring to (type) definitions and theorems easier, but note that it can also make [scoped instances], notations, and attributes from a different namespace available. The `open` command can be used in a few different ways: * `open Some.Namespace.Path1 Some.Namespace.Path2` makes all non-protected names in `Some.Namespace.Path1` and `Some.Namespace.Path2` available without the prefix, so that `Some.Namespace.Path1.x` and `Some.Namespace.Path2.y` can be referred to by writing only `x` and `y`. * `open Some.Namespace.Path hiding def1 def2` opens all non-protected names in `Some.Namespace.Path` except `def1` and `def2`. * `open Some.Namespace.Path (def1 def2)` only makes `Some.Namespace.Path.def1` and `Some.Namespace.Path.def2` available without the full prefix, so `Some.Namespace.Path.def3` would be unaffected. This works even if `def1` and `def2` are `protected`. * `open Some.Namespace.Path renaming def1 → def1', def2 → def2'` same as `open Some.Namespace.Path (def1 def2)` but `def1`/`def2`'s names are changed to `def1'`/`def2'`. This works even if `def1` and `def2` are `protected`. * `open scoped Some.Namespace.Path1 Some.Namespace.Path2` **only** opens [scoped instances], notations, and attributes from `Namespace1` and `Namespace2`; it does **not** make any other name available. * `open <any of the open shapes above> in` makes the names `open`-ed visible only in the next command or expression. [scoped instance]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html#scoped-instances (Scoped instances in Theorem Proving in Lean) ## Examples ```lean /-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/ namespace Combinator.Calculus def I (a : α) : α := a def K (a : α) : β → α := fun _ => a def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z) end Combinator.Calculus section -- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`, -- until the section ends open Combinator.Calculus theorem SKx_eq_K : S K x = I := rfl end -- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here) open Combinator.Calculus in theorem SKx_eq_K' : S K x = I := rfl section -- open only `S` and `K` under `Combinator.Calculus` open Combinator.Calculus (S K) theorem SKxy_eq_y : S K x y = y := rfl -- `I` is not in scope, we have to use its full path theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl end section open Combinator.Calculus renaming I → identity, K → konstant #check identity #check konstant end section open Combinator.Calculus hiding S #check I #check K end section namespace Demo inductive MyType | val namespace N1 scoped infix:68 " ≋ " => BEq.beq scoped instance : BEq MyType where beq _ _ := true def Alias := MyType end N1 end Demo -- bring `≋` and the instance in scope, but not `Alias` open scoped Demo.N1 #check Demo.MyType.val == Demo.MyType.val #check Demo.MyType.val ≋ Demo.MyType.val -- #check Alias -- unknown identifier 'Alias' end ```open 命令打开一个命名空间，使其内容在当前节范围内可用。打开命名空间有很多变体，为管理本地范围提供了灵活性。

syntaxOpening Namespaces

command ::= ...
    | Makes names from other namespaces visible without writing the namespace prefix.

Names that are made available with `open` are visible within the current `section` or `namespace`
block. This makes referring to (type) definitions and theorems easier, but note that it can also
make [scoped instances], notations, and attributes from a different namespace available.

The `open` command can be used in a few different ways:

* `open Some.Namespace.Path1 Some.Namespace.Path2` makes all non-protected names in
  `Some.Namespace.Path1` and `Some.Namespace.Path2` available without the prefix, so that
  `Some.Namespace.Path1.x` and `Some.Namespace.Path2.y` can be referred to by writing only `x` and
  `y`.

* `open Some.Namespace.Path hiding def1 def2` opens all non-protected names in `Some.Namespace.Path`
  except `def1` and `def2`.

* `open Some.Namespace.Path (def1 def2)` only makes `Some.Namespace.Path.def1` and
  `Some.Namespace.Path.def2` available without the full prefix, so `Some.Namespace.Path.def3` would
  be unaffected.

  This works even if `def1` and `def2` are `protected`.

* `open Some.Namespace.Path renaming def1 → def1', def2 → def2'` same as `open Some.Namespace.Path
  (def1 def2)` but `def1`/`def2`'s names are changed to `def1'`/`def2'`.

  This works even if `def1` and `def2` are `protected`.

* `open scoped Some.Namespace.Path1 Some.Namespace.Path2` **only** opens [scoped instances],
  notations, and attributes from `Namespace1` and `Namespace2`; it does **not** make any other name
  available.

* `open <any of the open shapes above> in` makes the names `open`-ed visible only in the next
  command or expression.

[scoped instance]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html#scoped-instances
(Scoped instances in Theorem Proving in Lean)


## Examples

```lean
/-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/
namespace Combinator.Calculus
  def I (a : α) : α := a
  def K (a : α) : β → α := fun _ => a
  def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z)
end Combinator.Calculus

section
  -- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`,
  -- until the section ends
  open Combinator.Calculus

  theorem SKx_eq_K : S K x = I := rfl
end

-- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here)
open Combinator.Calculus in
theorem SKx_eq_K' : S K x = I := rfl

section
  -- open only `S` and `K` under `Combinator.Calculus`
  open Combinator.Calculus (S K)

  theorem SKxy_eq_y : S K x y = y := rfl

  -- `I` is not in scope, we have to use its full path
  theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl
end

section
  open Combinator.Calculus
    renaming
      I → identity,
      K → konstant

  #check identity
  #check konstant
end

section
  open Combinator.Calculus
    hiding S

  #check I
  #check K
end

section
  namespace Demo
    inductive MyType
    | val

    namespace N1
      scoped infix:68 " ≋ " => BEq.beq

      scoped instance : BEq MyType where
        beq _ _ := true

      def Alias := MyType
    end N1
  end Demo

  -- bring `≋` and the instance in scope, but not `Alias`
  open scoped Demo.N1

  #check Demo.MyType.val == Demo.MyType.val
  #check Demo.MyType.val ≋ Demo.MyType.val
  -- #check Alias -- unknown identifier 'Alias'
end
```
open openDecl

open declarationOpening Entire Namespaces

一个或多个标识符的序列导致序列中的每个名称空间被打开：

`openDecl` is the body of an `open` declaration (see `open`) openDecl ::= ...
    | ident ident*

序列中的每个命名空间都被视为相对于所有当前打开的命名空间，从而产生一组命名空间。该集合中的每个命名空间都会在处理序列中的下一个命名空间之前打开。

Opening Nested Namespaces

要打开的命名空间被视为相对于当前打开的命名空间。如果相同的组件出现在不同的命名空间路径中，则可以使用单个 Lean.Parser.Command.open : commandMakes names from other namespaces visible without writing the namespace prefix. Names that are made available with `open` are visible within the current `section` or `namespace` block. This makes referring to (type) definitions and theorems easier, but note that it can also make [scoped instances], notations, and attributes from a different namespace available. The `open` command can be used in a few different ways: * `open Some.Namespace.Path1 Some.Namespace.Path2` makes all non-protected names in `Some.Namespace.Path1` and `Some.Namespace.Path2` available without the prefix, so that `Some.Namespace.Path1.x` and `Some.Namespace.Path2.y` can be referred to by writing only `x` and `y`. * `open Some.Namespace.Path hiding def1 def2` opens all non-protected names in `Some.Namespace.Path` except `def1` and `def2`. * `open Some.Namespace.Path (def1 def2)` only makes `Some.Namespace.Path.def1` and `Some.Namespace.Path.def2` available without the full prefix, so `Some.Namespace.Path.def3` would be unaffected. This works even if `def1` and `def2` are `protected`. * `open Some.Namespace.Path renaming def1 → def1', def2 → def2'` same as `open Some.Namespace.Path (def1 def2)` but `def1`/`def2`'s names are changed to `def1'`/`def2'`. This works even if `def1` and `def2` are `protected`. * `open scoped Some.Namespace.Path1 Some.Namespace.Path2` **only** opens [scoped instances], notations, and attributes from `Namespace1` and `Namespace2`; it does **not** make any other name available. * `open <any of the open shapes above> in` makes the names `open`-ed visible only in the next command or expression. [scoped instance]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html#scoped-instances (Scoped instances in Theorem Proving in Lean) ## Examples ```lean /-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/ namespace Combinator.Calculus def I (a : α) : α := a def K (a : α) : β → α := fun _ => a def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z) end Combinator.Calculus section -- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`, -- until the section ends open Combinator.Calculus theorem SKx_eq_K : S K x = I := rfl end -- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here) open Combinator.Calculus in theorem SKx_eq_K' : S K x = I := rfl section -- open only `S` and `K` under `Combinator.Calculus` open Combinator.Calculus (S K) theorem SKxy_eq_y : S K x y = y := rfl -- `I` is not in scope, we have to use its full path theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl end section open Combinator.Calculus renaming I → identity, K → konstant #check identity #check konstant end section open Combinator.Calculus hiding S #check I #check K end section namespace Demo inductive MyType | val namespace N1 scoped infix:68 " ≋ " => BEq.beq scoped instance : BEq MyType where beq _ _ := true def Alias := MyType end N1 end Demo -- bring `≋` and the instance in scope, but not `Alias` open scoped Demo.N1 #check Demo.MyType.val == Demo.MyType.val #check Demo.MyType.val ≋ Demo.MyType.val -- #check Alias -- unknown identifier 'Alias' end ```open 命令通过迭代地将每个组件纳入范围来打开所有组件。此示例定义了各种命名空间中的名称：

namespace A -- _root_.A
def a1 := 0
namespace B -- _root_.A.B
def a2 := 0
namespace C -- _root_.A.B.C
def a3 := 0
end C
end B
end A
namespace B -- _root_.B
def a4 := 0
namespace C -- _root_.B.C
def a5 := 0
end C
end B
namespace C -- _root_.C
def a6 := 0
end C

名字是：

A.a1
A.B.a2
A.B.C.a3
B.a4
B.C.a5
C.a6

可以使用单个迭代 Lean.Parser.Command.open : commandMakes names from other namespaces visible without writing the namespace prefix. Names that are made available with `open` are visible within the current `section` or `namespace` block. This makes referring to (type) definitions and theorems easier, but note that it can also make [scoped instances], notations, and attributes from a different namespace available. The `open` command can be used in a few different ways: * `open Some.Namespace.Path1 Some.Namespace.Path2` makes all non-protected names in `Some.Namespace.Path1` and `Some.Namespace.Path2` available without the prefix, so that `Some.Namespace.Path1.x` and `Some.Namespace.Path2.y` can be referred to by writing only `x` and `y`. * `open Some.Namespace.Path hiding def1 def2` opens all non-protected names in `Some.Namespace.Path` except `def1` and `def2`. * `open Some.Namespace.Path (def1 def2)` only makes `Some.Namespace.Path.def1` and `Some.Namespace.Path.def2` available without the full prefix, so `Some.Namespace.Path.def3` would be unaffected. This works even if `def1` and `def2` are `protected`. * `open Some.Namespace.Path renaming def1 → def1', def2 → def2'` same as `open Some.Namespace.Path (def1 def2)` but `def1`/`def2`'s names are changed to `def1'`/`def2'`. This works even if `def1` and `def2` are `protected`. * `open scoped Some.Namespace.Path1 Some.Namespace.Path2` **only** opens [scoped instances], notations, and attributes from `Namespace1` and `Namespace2`; it does **not** make any other name available. * `open <any of the open shapes above> in` makes the names `open`-ed visible only in the next command or expression. [scoped instance]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html#scoped-instances (Scoped instances in Theorem Proving in Lean) ## Examples ```lean /-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/ namespace Combinator.Calculus def I (a : α) : α := a def K (a : α) : β → α := fun _ => a def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z) end Combinator.Calculus section -- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`, -- until the section ends open Combinator.Calculus theorem SKx_eq_K : S K x = I := rfl end -- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here) open Combinator.Calculus in theorem SKx_eq_K' : S K x = I := rfl section -- open only `S` and `K` under `Combinator.Calculus` open Combinator.Calculus (S K) theorem SKxy_eq_y : S K x y = y := rfl -- `I` is not in scope, we have to use its full path theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl end section open Combinator.Calculus renaming I → identity, K → konstant #check identity #check konstant end section open Combinator.Calculus hiding S #check I #check K end section namespace Demo inductive MyType | val namespace N1 scoped infix:68 " ≋ " => BEq.beq scoped instance : BEq MyType where beq _ _ := true def Alias := MyType end N1 end Demo -- bring `≋` and the instance in scope, but not `Alias` open scoped Demo.N1 #check Demo.MyType.val == Demo.MyType.val #check Demo.MyType.val ≋ Demo.MyType.val -- #check Alias -- unknown identifier 'Alias' end ```open 命令将所有六个名称纳入范围：

section
open A B C
example := [a1, a2, a3, a4, a5, a6]
end

如果命令中的初始命名空间为 A.B，则 _root_.A、_root_.B 和 _root_.B.C 都不会打开：

section
open A.B C
example := [Unknown identifier `a1`a1, a2, a3, Unknown identifier `a4`a4, Unknown identifier `a5`a5, a6]
end

Unknown identifier `a1`

Unknown identifier `a4`

Unknown identifier `a5`

打开 A.B 会使 A.B.C 与 _root_.C 一起显示为 C，因此后续的 C 将打开两者。

Live ↪

open declarationHiding Names

hiding 声明指定一组不应纳入范围的名称。与打开整个命名空间相反，提供的标识符必须唯一指定要打开的命名空间。

`openDecl` is the body of an `open` declaration (see `open`) openDecl ::= ...
    | ident hiding ident ident*

open declarationRenaming

renaming 声明允许重命名打开的命名空间中的某些名称；它们可以在当前节范围内以新名称进行访问。提供的标识符必须唯一指定要打开的命名空间。

`openDecl` is the body of an `open` declaration (see `open`) openDecl ::= ...
    | ident renaming (ident → ident),*

可以使用ASCII箭头(->)代替Unicode箭头(→)。

open declarationRestricted Opening

括号表示仅括号中列出的名称应纳入范围。

`openDecl` is the body of an `open` declaration (see `open`) openDecl ::= ...
    | ident (ident ident*)

指示的命名空间将添加到每个当前打开的命名空间，并且每个名称都会在每个结果命名空间中考虑。所有列出的名称必须明确；也就是说，它们必须恰好存在于所考虑的命名空间之一中。

open declarationScoped Declarations Only

scoped 关键字指示应打开所提供命名空间中的所有作用域属性、实例和语法，同时不使任何名称可用。

`openDecl` is the body of an `open` declaration (see `open`) openDecl ::= ...
    | scoped ident ident*

Opening Scoped Declarations

在此示例中，在命名空间 NS 中创建作用域 notation 和定义：

namespace NS
scoped notation "{!{" e "}!}" => (e, e)
def three := 3
end NS

在命名空间之外，该表示法不可用：

def x := {!{ "pear" }unexpected token '!'; expected '}'!}

<example>:1:21-1:22: unexpected token '!'; expected '}'

open scoped 命令使符号可用：

open scoped NS
def x := {!{ "pear" }!}

但是，名称 NS.three 不在范围内：

def y := Unknown identifier `three`three

Unknown identifier `three`

Live ↪

6.1.2. 导出名称🔗

Exporting 名称使其在当前命名空间中可用。与定义不同，此别名是完全透明的：使用直接解析为原始名称。将名称导出到根命名空间使其无需限定即可使用； Lean 标准库对 Option 的构造函数等名称和 get 等键类型类方法执行此操作。

syntaxExporting Names

export 命令将其他名称空间中的名称添加到当前名称空间中，就像它们已在其中声明一样。当当前命名空间打开时，这些导出的名称也会进入作用域。

command ::= ...
    | Adds names from other namespaces to the current namespace.

The command `export Some.Namespace (name₁ name₂)` makes `name₁` and `name₂`:

- visible in the current namespace without prefix `Some.Namespace`, like `open`, and
- visible from outside the current namespace `N` as `N.name₁` and `N.name₂`.

## Examples

```lean
namespace Morning.Sky
  def star := "venus"
end Morning.Sky

namespace Evening.Sky
  export Morning.Sky (star)
  -- `star` is now in scope
  #check star
end Evening.Sky

-- `star` is visible in `Evening.Sky`
#check Evening.Sky.star
```
export ident (ident*)

在内部，导出的名称被注册为其目标的别名。从内核的角度来看，只存在原来的名称；精化器将别名解析为解析标识符的一部分。

Exported Names

归纳类型 Veg.Leafy 的声明建立了构造函数 Veg.Leafy.spinach 和 Veg.Leafy.cabbage：

namespace Veg
inductive Leafy where
  | spinach
  | cabbage
export Leafy (spinach)
end Veg
export Veg.Leafy (cabbage)

第一个 export 命令使 Veg.Leafy.spinach 可作为 Veg.spinach 进行访问，因为当前命名空间是 Veg。第二个使 Veg.Leafy.cabbage 可作为 cabbage 进行访问，因为当前命名空间是根命名空间。

Live ↪

6.2. 章节范围🔗

许多命令对当前 sectionscope 产生影响（有时在清除时简称为“scope”）。每个 Lean 模块都有一个部分范围。嵌套作用域是通过 Lean.Parser.Command.namespace : command`namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside the section: * Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the full name `Nat.seventeen`. * Names introduced by `export` declarations are also prefixed by the identifier. * All names starting with `<id>.` become available in the namespace without the prefix. These names are preferred over names introduced by outer namespaces or `open`. * Within a namespace, declarations can be `protected`, which excludes them from the effects of opening the namespace. As with `section`, namespaces can be nested and the scope of a namespace is terminated by a corresponding `end <id>` or the end of the file. `namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.namespace 和 Lean.Parser.Command.section : commandA `section`/`end` pair delimits the scope of `variable`, `include`, `open`, `set_option`, and `local` commands. Sections can be nested. `section <id>` provides a label to the section that has to appear with the matching `end`. In either case, the `end` can be omitted, in which case the section is closed at the end of the file.section 命令以及 Lean.Parser.Command.in : commandin 命令组合器创建的。

在部分范围内跟踪以下数据：

当前命名空间: 当前命名空间 是将在其中定义新声明的命名空间。此外，名称解析包括全局名称范围内当前命名空间的所有前缀。
开放的命名空间: 当命名空间为 opened 时，其名称在当前作用域中无需显式前缀即可使用。此外，已打开的命名空间中的作用域属性和作用域语法扩展在当前节作用域中处于活动状态。
选项: 编译器选项在修改范围结束时将恢复为其原始值。
节变量: 节变量是作为参数自动添加到定义中的名称（或实例隐式参数）。当它们出现在定理的陈述中时，它们也会作为全称量化的假设添加到定理中。

6.2.1. 控制部分范围🔗

Lean.Parser.Command.section : commandA `section`/`end` pair delimits the scope of `variable`, `include`, `open`, `set_option`, and `local` commands. Sections can be nested. `section <id>` provides a label to the section that has to appear with the matching `end`. In either case, the `end` can be omitted, in which case the section is closed at the end of the file.section 命令创建新的 section 范围，但不会修改当前命名空间、打开的命名空间或节变量。当节结束时，对节范围所做的更改将被恢复。此外，节可能会导致默认情况下将一组修饰符应用于该节中的所有声明。可以选择对节进行命名；关闭命名节的 Lean.Parser.Command.end : command`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed with `end <id>`. The `end` command is optional at the end of a file.end 命令必须使用相同的名称。如果节名称具有多个组成部分（即，如果它们包含 . 分隔的名称），则会引入多个嵌套节。节名称没有其他作用，并且有助于提高可读性。

syntaxSections

command ::= ...
    | A `section`/`end` pair delimits the scope of `variable`, `include`, `open`, `set_option`, and `local`
commands. Sections can be nested. `section <id>` provides a label to the section that has to appear
with the matching `end`. In either case, the `end` can be omitted, in which case the section is
closed at the end of the file.
sectionHeader section ident?

syntaxSection Headers

节标题（如果存在）会修改节中的声明。

sectionHeader ::= ...
    | (@[expose])?
      public? noncomputable? meta?

如果标头包含 noncomputable，则该节中的定义都被认为是不可计算的，并且不会为它们生成编译代码。这对于依赖非计算推理原则（例如选择公理）的定义是必需的。

其余修饰符仅在模块中有用。如果标头包含 @[expose]，则该节中的所有定义都是 exposed。如果它包含 public，则默认情况下，此类 publicsection 中的声明是公共的，而不是私有的。如果它包含meta，则该节的声明全部放在元阶段中。

Named Section

名称 english 在 Greetings 命名空间中定义。

def Greetings.english := "Hello"

在其名称空间之外，无法对其进行求值。

#eval Unknown identifier `english`english

Unknown identifier `english`

打开一个节可以包含对全局范围的修改。此部分名为 Greetings。

section Greetings

即使节名称与定义的名称空间匹配，该名称也不在范围内，因为节名称纯粹是为了可读性和易于重构。

#eval Unknown identifier `english`english

Unknown identifier `english`

打开命名空间 Greetings 会将 Greetings.english 变为 english：

open Greetings

"Hello"#eval english

"Hello"

必须使用该部分的名称来关闭它。

Missing name after `end`: Expected the current scope name `Greetings`

Hint: To end the current scope `Greetings`, specify its name:
  end ̲G̲r̲e̲e̲t̲i̲n̲g̲s̲end

Missing name after `end`: Expected the current scope name `Greetings`

Hint: To end the current scope `Greetings`, specify its name:
  end ̲G̲r̲e̲e̲t̲i̲n̲g̲s̲

end Greetings

当该部分关闭时，Lean.Parser.Command.open : commandMakes names from other namespaces visible without writing the namespace prefix. Names that are made available with `open` are visible within the current `section` or `namespace` block. This makes referring to (type) definitions and theorems easier, but note that it can also make [scoped instances], notations, and attributes from a different namespace available. The `open` command can be used in a few different ways: * `open Some.Namespace.Path1 Some.Namespace.Path2` makes all non-protected names in `Some.Namespace.Path1` and `Some.Namespace.Path2` available without the prefix, so that `Some.Namespace.Path1.x` and `Some.Namespace.Path2.y` can be referred to by writing only `x` and `y`. * `open Some.Namespace.Path hiding def1 def2` opens all non-protected names in `Some.Namespace.Path` except `def1` and `def2`. * `open Some.Namespace.Path (def1 def2)` only makes `Some.Namespace.Path.def1` and `Some.Namespace.Path.def2` available without the full prefix, so `Some.Namespace.Path.def3` would be unaffected. This works even if `def1` and `def2` are `protected`. * `open Some.Namespace.Path renaming def1 → def1', def2 → def2'` same as `open Some.Namespace.Path (def1 def2)` but `def1`/`def2`'s names are changed to `def1'`/`def2'`. This works even if `def1` and `def2` are `protected`. * `open scoped Some.Namespace.Path1 Some.Namespace.Path2` **only** opens [scoped instances], notations, and attributes from `Namespace1` and `Namespace2`; it does **not** make any other name available. * `open <any of the open shapes above> in` makes the names `open`-ed visible only in the next command or expression. [scoped instance]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html#scoped-instances (Scoped instances in Theorem Proving in Lean) ## Examples ```lean /-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/ namespace Combinator.Calculus def I (a : α) : α := a def K (a : α) : β → α := fun _ => a def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z) end Combinator.Calculus section -- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`, -- until the section ends open Combinator.Calculus theorem SKx_eq_K : S K x = I := rfl end -- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here) open Combinator.Calculus in theorem SKx_eq_K' : S K x = I := rfl section -- open only `S` and `K` under `Combinator.Calculus` open Combinator.Calculus (S K) theorem SKxy_eq_y : S K x y = y := rfl -- `I` is not in scope, we have to use its full path theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl end section open Combinator.Calculus renaming I → identity, K → konstant #check identity #check konstant end section open Combinator.Calculus hiding S #check I #check K end section namespace Demo inductive MyType | val namespace N1 scoped infix:68 " ≋ " => BEq.beq scoped instance : BEq MyType where beq _ _ := true def Alias := MyType end N1 end Demo -- bring `≋` and the instance in scope, but not `Alias` open scoped Demo.N1 #check Demo.MyType.val == Demo.MyType.val #check Demo.MyType.val ≋ Demo.MyType.val -- #check Alias -- unknown identifier 'Alias' end ```open 命令的效果将恢复。

#eval Unknown identifier `english`english

Unknown identifier `english`

Live ↪

Lean.Parser.Command.namespace : command`namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside the section: * Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the full name `Nat.seventeen`. * Names introduced by `export` declarations are also prefixed by the identifier. * All names starting with `<id>.` become available in the namespace without the prefix. These names are preferred over names introduced by outer namespaces or `open`. * Within a namespace, declarations can be `protected`, which excludes them from the effects of opening the namespace. As with `section`, namespaces can be nested and the scope of a namespace is terminated by a corresponding `end <id>` or the end of the file. `namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.namespace 命令创建新的节范围。在此节范围内，当前命名空间是命令中提供的名称，相对于周围节范围中的当前命名空间进行解释。与节一样，当命名空间的范围结束时，对节范围所做的更改将被恢复。

要关闭命名空间，Lean.Parser.Command.end : command`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed with `end <id>`. The `end` command is optional at the end of a file.end 命令需要当前命名空间的后缀，该后缀已被删除。由引入该后缀部分的 Lean.Parser.Command.namespace : command`namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside the section: * Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the full name `Nat.seventeen`. * Names introduced by `export` declarations are also prefixed by the identifier. * All names starting with `<id>.` become available in the namespace without the prefix. These names are preferred over names introduced by outer namespaces or `open`. * Within a namespace, declarations can be `protected`, which excludes them from the effects of opening the namespace. As with `section`, namespaces can be nested and the scope of a namespace is terminated by a corresponding `end <id>` or the end of the file. `namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.namespace 命令引入的所有节范围均已关闭。

syntaxNamespace Declarations

namespace 命令通过附加提供的标识符来修改当前命名空间。它创建一个持续到 Lean.Parser.Command.end : command`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed with `end <id>`. The `end` command is optional at the end of a file.end 命令或文件末尾的节范围。

command ::= ...
    | `namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside
the section:
* Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the
  full name `Nat.seventeen`.
* Names introduced by `export` declarations are also prefixed by the identifier.
* All names starting with `<id>.` become available in the namespace without the prefix. These names
  are preferred over names introduced by outer namespaces or `open`.
* Within a namespace, declarations can be `protected`, which excludes them from the effects of
  opening the namespace.

As with `section`, namespaces can be nested and the scope of a namespace is terminated by a
corresponding `end <id>` or the end of the file.

`namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.
namespace ident

syntaxSection and Namespace Terminators

如果没有标识符，Lean.Parser.Command.end : command`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed with `end <id>`. The `end` command is optional at the end of a file.end 会关闭最近打开的部分，该部分必须是匿名的。

command ::= ...
    | `end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed
with `end <id>`. The `end` command is optional at the end of a file.
end

使用标识符，它关闭最近打开的部分或名称空间。如果它是一个节，则标识符必须是自最近的 Lean.Parser.Command.namespace : command`namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside the section: * Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the full name `Nat.seventeen`. * Names introduced by `export` declarations are also prefixed by the identifier. * All names starting with `<id>.` become available in the namespace without the prefix. These names are preferred over names introduced by outer namespaces or `open`. * Within a namespace, declarations can be `protected`, which excludes them from the effects of opening the namespace. As with `section`, namespaces can be nested and the scope of a namespace is terminated by a corresponding `end <id>` or the end of the file. `namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.namespace 命令以来打开的节的串联名称的后缀。如果它是命名空间，则标识符必须是自最新仍打开的 Lean.Parser.Command.section : commandA `section`/`end` pair delimits the scope of `variable`, `include`, `open`, `set_option`, and `local` commands. Sections can be nested. `section <id>` provides a label to the section that has to appear with the matching `end`. In either case, the `end` can be omitted, in which case the section is closed at the end of the file.section 以来的当前命名空间扩展的后缀；之后，当前命名空间将删除此后缀。

command ::= ...
    | `end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed
with `end <id>`. The `end` command is optional at the end of a file.
end ident

关闭 Lean.Parser.Command.mutual : commandmutual 块的 Lean.Parser.Command.mutual : commandend 是 Lean.Parser.Command.mutual : commandmutual 语法的一部分，而不是 Lean.Parser.Command.end : command`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed with `end <id>`. The `end` command is optional at the end of a file.end 命令。

Nesting Namespaces and Sections

命名空间和节可以嵌套。单个 Lean.Parser.Command.end : command`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed with `end <id>`. The `end` command is optional at the end of a file.end 命令可以关闭一个或多个命名空间或一个或多个部分，但不能关闭两者的混合。

使用两个单独的命令将当前命名空间设置为 A.B.C 后，可以使用单个 Lean.Parser.Command.end : command`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed with `end <id>`. The `end` command is optional at the end of a file.end 删除 B.C：

namespace A.B
namespace C
end B.C

此时，当前命名空间为A。

接下来，打开一个匿名部分和命名空间 D.E：

section
namespace D.E

此时，当前命名空间为A.D.E。由于中间部分，Lean.Parser.Command.end : command`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed with `end <id>`. The `end` command is optional at the end of a file.end 命令无法关闭所有三个命令：

Invalid name after `end`: Expected `D.E`, but found `A.D.E`end A.D.E

Invalid name after `end`: Expected `D.E`, but found `A.D.E`

相反，命名空间和节必须单独结束。

end D.E
end
end A

Live ↪

Lean.Parser.Command.in : commandin 组合器可用于创建单命令节范围，而不是为单个命令打开节。 Lean.Parser.Command.in : commandin 组合器是右关联的，允许堆叠多个范围修改。

syntaxLocal Section Scopes

in 命令组合器引入了单个命令的节范围。

command ::= ...
    | command in
      command

Using Lean.Parser.Command.in : commandin for Local Scopes

使用 Lean.Parser.Command.in : commandin 可以使命名空间的内容可供单个命令使用。

def Dessert.cupcake := "delicious"

open Dessert in
"delicious"#eval cupcake

单个命令后，Lean.Parser.Command.open : commandMakes names from other namespaces visible without writing the namespace prefix. Names that are made available with `open` are visible within the current `section` or `namespace` block. This makes referring to (type) definitions and theorems easier, but note that it can also make [scoped instances], notations, and attributes from a different namespace available. The `open` command can be used in a few different ways: * `open Some.Namespace.Path1 Some.Namespace.Path2` makes all non-protected names in `Some.Namespace.Path1` and `Some.Namespace.Path2` available without the prefix, so that `Some.Namespace.Path1.x` and `Some.Namespace.Path2.y` can be referred to by writing only `x` and `y`. * `open Some.Namespace.Path hiding def1 def2` opens all non-protected names in `Some.Namespace.Path` except `def1` and `def2`. * `open Some.Namespace.Path (def1 def2)` only makes `Some.Namespace.Path.def1` and `Some.Namespace.Path.def2` available without the full prefix, so `Some.Namespace.Path.def3` would be unaffected. This works even if `def1` and `def2` are `protected`. * `open Some.Namespace.Path renaming def1 → def1', def2 → def2'` same as `open Some.Namespace.Path (def1 def2)` but `def1`/`def2`'s names are changed to `def1'`/`def2'`. This works even if `def1` and `def2` are `protected`. * `open scoped Some.Namespace.Path1 Some.Namespace.Path2` **only** opens [scoped instances], notations, and attributes from `Namespace1` and `Namespace2`; it does **not** make any other name available. * `open <any of the open shapes above> in` makes the names `open`-ed visible only in the next command or expression. [scoped instance]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html#scoped-instances (Scoped instances in Theorem Proving in Lean) ## Examples ```lean /-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/ namespace Combinator.Calculus def I (a : α) : α := a def K (a : α) : β → α := fun _ => a def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z) end Combinator.Calculus section -- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`, -- until the section ends open Combinator.Calculus theorem SKx_eq_K : S K x = I := rfl end -- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here) open Combinator.Calculus in theorem SKx_eq_K' : S K x = I := rfl section -- open only `S` and `K` under `Combinator.Calculus` open Combinator.Calculus (S K) theorem SKxy_eq_y : S K x y = y := rfl -- `I` is not in scope, we have to use its full path theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl end section open Combinator.Calculus renaming I → identity, K → konstant #check identity #check konstant end section open Combinator.Calculus hiding S #check I #check K end section namespace Demo inductive MyType | val namespace N1 scoped infix:68 " ≋ " => BEq.beq scoped instance : BEq MyType where beq _ _ := true def Alias := MyType end N1 end Demo -- bring `≋` and the instance in scope, but not `Alias` open scoped Demo.N1 #check Demo.MyType.val == Demo.MyType.val #check Demo.MyType.val ≋ Demo.MyType.val -- #check Alias -- unknown identifier 'Alias' end ```open 的效果恢复。

#eval Unknown identifier `cupcake`cupcake

Unknown identifier `cupcake`

Live ↪

6.2.2. 节变量🔗

Section Variables 是自动添加到提及它们的声明中的参数。无论选项 autoImplicit 是否为 true，都会发生这种情况。节变量可以是隐式的、严格隐式的或显式的；实例隐式节变量经过特殊处理。

当在非定理声明中遇到节变量的名称时，会将其添加为参数。还会添加提及该变量的任何实例隐式节变量。如果添加的任何变量依赖于其他变量，那么这些变量也会被添加；迭代此过程，直到不再有依赖关系为止。所有节变量都按照声明顺序添加到所有其他参数之前。仅当节变量出现在定理的陈述中时才会添加节变量。否则，如果证明项使用了节变量，则修改定理的证明可能会更改其陈述。

使用 Lean.Parser.Command.variable : commandDeclares one or more typed variables, or modifies whether already-declared variables are implicit. Introduces variables that can be used in definitions within the same `namespace` or `section` block. When a definition mentions a variable, Lean will add it as an argument of the definition. This is useful in particular when writing many definitions that have parameters in common (see below for an example). Variable declarations have the same flexibility as regular function parameters. In particular they can be [explicit, implicit][binder docs], or [instance implicit][tpil classes] (in which case they can be anonymous). This can be changed, for instance one can turn explicit variable `x` into an implicit one with `variable {x}`. Note that currently, you should avoid changing how variables are bound and declare new variables at the same time; see [issue 2789] for more on this topic. In *theorem bodies* (i.e. proofs), variables are not included based on usage in order to ensure that changes to the proof cannot change the statement of the overall theorem. Instead, variables are only available to the proof if they have been mentioned in the theorem header or in an `include` command or are instance implicit and depend only on such variables. See [*Variables and Sections* from Theorem Proving in Lean][tpil vars] for a more detailed discussion. [tpil vars]: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#variables-and-sections (Variables and Sections on Theorem Proving in Lean) [tpil classes]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html (Type classes on Theorem Proving in Lean) [binder docs]: https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.BinderInfo (Documentation for the BinderInfo type) [issue 2789]: https://github.com/leanprover/lean4/issues/2789 (Issue 2789 on github) ## Examples ```lean section variable {α : Type u} -- implicit (a : α) -- explicit [instBEq : BEq α] -- instance implicit, named [Hashable α] -- instance implicit, anonymous def isEqual (b : α) : Bool := a == b #check isEqual -- isEqual.{u} {α : Type u} (a : α) [instBEq : BEq α] (b : α) : Bool variable {a} -- `a` is implicit now def eqComm {b : α} := a == b ↔ b == a #check eqComm -- eqComm.{u} {α : Type u} {a : α} [instBEq : BEq α] {b : α} : Prop end ``` The following shows a typical use of `variable` to factor out definition arguments: ```lean variable (Src : Type) structure Logger where trace : List (Src × String) #check Logger -- Logger (Src : Type) : Type namespace Logger -- switch `Src : Type` to be implicit until the `end Logger` variable {Src} def empty : Logger Src where trace := [] #check empty -- Logger.empty {Src : Type} : Logger Src variable (log : Logger Src) def len := log.trace.length #check len -- Logger.len {Src : Type} (log : Logger Src) : Nat variable (src : Src) [BEq Src] -- at this point all of `log`, `src`, `Src` and the `BEq` instance can all become arguments def filterSrc := log.trace.filterMap fun (src', str') => if src' == src then some str' else none #check filterSrc -- Logger.filterSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : List String def lenSrc := log.filterSrc src |>.length #check lenSrc -- Logger.lenSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : Nat end Logger ``` The following example demonstrates availability of variables in proofs: ```lean variable {α : Type} -- available in the proof as indirectly mentioned through `a` [ToString α] -- available in the proof as `α` is included (a : α) -- available in the proof as mentioned in the header {β : Type} -- not available in the proof [ToString β] -- not available in the proof theorem ex : a = a := rfl ``` After elaboration of the proof, the following warning will be generated to highlight the unused hypothesis: ``` included section variable '[ToString α]' is not used in 'ex', consider excluding it ``` In such cases, the offending variable declaration should be moved down or into a section so that only theorems that do depend on it follow it until the end of the section.variable 命令声明变量。

syntaxVariable Declarations

command ::= ...
    | Declares one or more typed variables, or modifies whether already-declared variables are
  implicit.

Introduces variables that can be used in definitions within the same `namespace` or `section` block.
When a definition mentions a variable, Lean will add it as an argument of the definition. This is
useful in particular when writing many definitions that have parameters in common (see below for an
example).

Variable declarations have the same flexibility as regular function parameters. In particular they
can be [explicit, implicit][binder docs], or [instance implicit][tpil classes] (in which case they
can be anonymous). This can be changed, for instance one can turn explicit variable `x` into an
implicit one with `variable {x}`. Note that currently, you should avoid changing how variables are
bound and declare new variables at the same time; see [issue 2789] for more on this topic.

In *theorem bodies* (i.e. proofs), variables are not included based on usage in order to ensure that
changes to the proof cannot change the statement of the overall theorem. Instead, variables are only
available to the proof if they have been mentioned in the theorem header or in an `include` command
or are instance implicit and depend only on such variables.

See [*Variables and Sections* from Theorem Proving in Lean][tpil vars] for a more detailed
discussion.

[tpil vars]:
https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#variables-and-sections
(Variables and Sections on Theorem Proving in Lean) [tpil classes]:
https://lean-lang.org/theorem_proving_in_lean4/type_classes.html (Type classes on Theorem Proving in
Lean) [binder docs]:
https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.BinderInfo (Documentation
for the BinderInfo type) [issue 2789]: https://github.com/leanprover/lean4/issues/2789 (Issue 2789
on github)

## Examples

```lean
section
  variable
    {α : Type u}      -- implicit
    (a : α)           -- explicit
    [instBEq : BEq α] -- instance implicit, named
    [Hashable α]      -- instance implicit, anonymous

  def isEqual (b : α) : Bool :=
    a == b

  #check isEqual
  -- isEqual.{u} {α : Type u} (a : α) [instBEq : BEq α] (b : α) : Bool

  variable
    {a} -- `a` is implicit now

  def eqComm {b : α} := a == b ↔ b == a

  #check eqComm
  -- eqComm.{u} {α : Type u} {a : α} [instBEq : BEq α] {b : α} : Prop
end
```

The following shows a typical use of `variable` to factor out definition arguments:

```lean
variable (Src : Type)

structure Logger where
  trace : List (Src × String)
#check Logger
-- Logger (Src : Type) : Type

namespace Logger
  -- switch `Src : Type` to be implicit until the `end Logger`
  variable {Src}

  def empty : Logger Src where
    trace := []
  #check empty
  -- Logger.empty {Src : Type} : Logger Src

  variable (log : Logger Src)

  def len :=
    log.trace.length
  #check len
  -- Logger.len {Src : Type} (log : Logger Src) : Nat

  variable (src : Src) [BEq Src]

  -- at this point all of `log`, `src`, `Src` and the `BEq` instance can all become arguments

  def filterSrc :=
    log.trace.filterMap
      fun (src', str') => if src' == src then some str' else none
  #check filterSrc
  -- Logger.filterSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : List String

  def lenSrc :=
    log.filterSrc src |>.length
  #check lenSrc
  -- Logger.lenSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : Nat
end Logger
```

The following example demonstrates availability of variables in proofs:
```lean
variable
  {α : Type}    -- available in the proof as indirectly mentioned through `a`
  [ToString α]  -- available in the proof as `α` is included
  (a : α)       -- available in the proof as mentioned in the header
  {β : Type}    -- not available in the proof
  [ToString β]  -- not available in the proof

theorem ex : a = a := rfl
```
After elaboration of the proof, the following warning will be generated to highlight the unused
hypothesis:
```
included section variable '[ToString α]' is not used in 'ex', consider excluding it
```
In such cases, the offending variable declaration should be moved down or into a section so that
only theorems that do depend on it follow it until the end of the section.
variable bracketedBinder bracketedBinder*

variable 后允许的括号内的绑定符与定义标头中使用的语法匹配。

Section Variables

在本节中，自动隐式参数被禁用，但定义了许多节变量。

section
set_option autoImplicit false
universe u
variable {α : Type u} (xs : List α) [Zero α] [Add α]

由于自动隐式参数已禁用，并且 β 既不是节变量也不是绑定为函数的参数，因此以下定义失败：

def addAll (lst : List Unknown identifier `β`

Note: It is not possible to treat `β` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.β) : Unknown identifier `β`

Note: It is not possible to treat `β` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.β :=
  lst.foldr (init := 0) (· + ·)

Unknown identifier `β`

Note: It is not possible to treat `β` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.

另一方面，当使用节变量时，甚至 xs 也不需要直接写入定义中：

def addAll :=
  xs.foldr (init := 0) (· + ·)

Live ↪

要向定理添加节变量（即使语句中未明确提及），请使用 Lean.Parser.Command.include : command`include eeny meeny` instructs Lean to include the section `variable`s `eeny` and `meeny` in all theorems in the remainder of the current section, differing from the default behavior of conditionally including variables based on use in the theorem header. Other commands are not affected. `include` is usually followed by `in theorem ...` to limit the inclusion to the subsequent declaration.include 命令标记该变量。所有标记为包含的变量都将添加到所有定理中。 Lean.Parser.Command.omit : command`omit` instructs Lean to not include a variable previously `include`d. Apart from variable names, it can also refer to typeclass instance variables by type using the syntax `omit [TypeOfInst]`, in which case all instance variables that unify with the given type are omitted. `omit` should usually only be used in conjunction with `in` in order to keep the section structure simple.omit 命令从变量中删除包含标记；将其与 Lean.Parser.Command.in : commandin 一起使用通常是个好主意。

Included and Omitted Section Variables

本节的变量包括一个谓词以及证明它普遍成立所需的一切，以及一个无用的额外假设。

section
variable {p : Nat → Prop}
variable (pZero : p 0) (pStep : ∀ n, p n → p (n + 1))
variable (pFifteen : p 15)

然而，该定理的假设中仅添加了p，因此无法证明。

theorem p_all : ∀ n, p n := unsolved goals
zerop:Nat → Prop⊢ p 0

succp:Nat → Propn✝:Nata✝:p n✝⊢ p (n✝ + 1)byp:Nat → Prop⊢ ∀ (n : Nat), p n
  intro np:Nat → Propn:Nat⊢ p n
  induction nzerop:Nat → Prop⊢ p 0succp:Nat → Propn✝:Nata✝:p n✝⊢ p (n✝ + 1)

Lean.Parser.Command.include : command`include eeny meeny` instructs Lean to include the section `variable`s `eeny` and `meeny` in all theorems in the remainder of the current section, differing from the default behavior of conditionally including variables based on use in the theorem header. Other commands are not affected. `include` is usually followed by `in theorem ...` to limit the inclusion to the subsequent declaration.include 命令导致无条件添加附加假设：

include pZero pStep pFifteen

automatically included section variable(s) unused in theorem `p_all`:
  pFifteen
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit pFifteen in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`theorem p_all : ∀ n, p n := byp✝:Nat → ProppFifteen:p✝ 15p:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)⊢ ∀ (n : Nat), p n
  intro np✝:Nat → ProppFifteen:p✝ 15p:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)n:Nat⊢ p n
  induction nzerop✝:Nat → ProppFifteen:p✝ 15p:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)⊢ p 0succp✝:Nat → ProppFifteen:p✝ 15p:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)n✝:Nata✝:p n✝⊢ p (n✝ + 1) <;>zerop✝:Nat → ProppFifteen:p✝ 15p:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)⊢ p 0succp✝:Nat → ProppFifteen:p✝ 15p:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)n✝:Nata✝:p n✝⊢ p (n✝ + 1) simp [*]All goals completed! 🐙

由于插入了虚假假设 pFifteen，Lean 发出警告：

automatically included section variable(s) unused in theorem `p_all`:
  pFifteen
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit pFifteen in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`

通过使用 Lean.Parser.Command.omit : command`omit` instructs Lean to not include a variable previously `include`d. Apart from variable names, it can also refer to typeclass instance variables by type using the syntax `omit [TypeOfInst]`, in which case all instance variables that unify with the given type are omitted. `omit` should usually only be used in conjunction with `in` in order to keep the section structure simple.omit 删除 pFifteen 可以避免这种情况：

include pZero pStep pFifteen

omit pFifteen in
theorem p_all : ∀ n, p n := byp:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)⊢ ∀ (n : Nat), p n
  intro np:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)n:Nat⊢ p n
  induction nzerop:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)⊢ p 0succp:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)n✝:Nata✝:p n✝⊢ p (n✝ + 1) <;>zerop:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)⊢ p 0succp:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)n✝:Nata✝:p n✝⊢ p (n✝ + 1) simp [*]All goals completed! 🐙

end

Live ↪