# 翻译-Lean Language Reference-06-命名空间和区段

{{< ctxset prefix="6" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="术语" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="语法" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="常量" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="定理" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="公理" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="归纳" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="结构" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="类型类" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="选项" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="属性" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="例子" cnt_sect_lv_max="2">}}

Lean 里的名称会被组织到分层的{{< labelindex 
  type="术语" 
  id_alias="命名空间"
  title_alias="命名空间 Namespace"
>}}
{{< /labelindex >}}**命名空间 Namespace** 中。
命名空间是名称的集合，它们是 Lean 组织 API 的主要手段。
命名空间提供了操作的本体论，将相关项目组织到一起；此外如
  [扩展记号](https://lean-lang.org/doc/reference/latest/Notations-and-Macros/#language-extension)、
  [实例](https://lean-lang.org/doc/reference/latest/Type-Classes/#--tech-term-instances)、
  [属性](https://lean-lang.org/doc/reference/latest/Attributes/#--tech-term-Attributes)
等功能的效果也可以被附加到命名空间上，
尽管这并不是通过在命名空间中为它们命名来实现的。

我们可以将操作整理到命名空间中以便从全局角度对库进行概念上的组织；
然而在通常情况下，任何给定的 Lean 文件都不会同等地使用所有名称。 
[区段](#术语-区段)提供了
  一种可以对全局可用名称集合在局部视图下进行排序的方法，以及
  一种可以精确控制编译器选项、语言扩展、实例和属性的作用域的手段。
区段还允许那些被许多函数常量声明所共享的形参
  可以被集中声明，并且
  可以通过 `variable` 命令被按需传播。

## 6.1. 命名空间 Namespaces {#S6-1}
{{< ctx level="2" >}}

那些包含点号且没有被[法语引号](https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules/#--tech-term-guillemets)包裹的名称是分层名称；
点号用于分隔名称的{{< labelindex 
  type="术语" 
  id_alias="名称组件"
  title_alias="名称组件 Component"
>}}
{{< /labelindex >}}**组件 Component**。
除了最后一个组件是名称本身之外，名称的所有组件都是命名空间。

命名空间用于将相关的定义、定理、类型以及其他声明组织起来。
如果一个命名空间的名称正好对应于一个类型，
那么其中的内容就可通过广义字段表示法访问。
除了名称之外，命名空间还可以用于组织
  [扩展记号](https://lean-lang.org/doc/reference/latest/Notations-and-Macros/#language-extension)、
  [属性](https://lean-lang.org/doc/reference/latest/Attributes/#--tech-term-Attributes)以及
  [类型类实例](https://lean-lang.org/doc/reference/latest/Type-Classes/#--tech-term-instances)。

命名空间与[模块](https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules/#--tech-term-module)是正交的：
模块是一个代码单元，里面的内容会被一起阐述、编译和加载，但是
模块本身的名称与模块所提供的名称之间并没有必要的联系。
模块可以包含任何命名空间中的名称，并且
分层模块的嵌套结构与分层命名空间的嵌套结构无关。

Lean 里有一个根部命名空间，要表示它
  通常只需要省略命名空间名称即可，
  或者也可以通过在名称前加上 `_root_` 来显式书写。
后者在某些情况下是必须的，否则
名称的解释就会按照相对于一个
  （可能来自于[区段作用域](#术语-区段作用域)的）环境命名空间或一个
  局部作用域
进行处理。

{{< labelindex 
  type="例子" 
  summary="根部命名空间的显式表示"
>}}
示范：`Forest`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：根部命名空间的显式表示" 
  open=false
>}}
当前命名空间中的名称优先级高于根部命名空间中的名称。在下述例子中，
`Forest.statement` 的声明中提到的 `color` 指向的是 `Forest.color`：

```lean {wrapper=false, lineNos=false}
def color := "yellow" -- _root_.color
namespace Forest
def color := "green"  -- _root_.Forest.color
def statement := s!"Lemons are {color}"
end Forest
#eval Forest.statement
-- "Lemons are green"
```

要想在 `Forest` 命名空间中调用根部命名空间中的 `color`
就必须使用 `_root_` 来限定作用域：

```lean {wrapper=false, lineNos=false}
namespace Forest
def nextStatement :=
  s!"Ripe lemons are {_root_.color}, not {color}"
end Forest
#eval Forest.nextStatement
-- "Ripe lemons are yellow, not green"
```
{{< /admonition >}}

### 6.1.1. 命名空间与区段作用域 Namespaces and Section Scopes {#S6-1-1}
{{< ctx level="3" >}}

每个[区段作用域](#术语-区段作用域)都有一个[当前命名空间](#术语-当前命名空间)，
后者由 `namespace` 命令所决定。

> `namespace` 命令的详细介绍请查阅[“作用域命令”](#S6-2-1)一节。

区段作用域中声明的名称都会被添加到当前命名空间中。
如果已声明的名称拥有多个组件，那么它的命名空间就会被嵌套进当前命名空间中；
此时声明主体所处的当前命名空间就会变成嵌套的命名空间。
区段作用域还包括一系列已开启的命名空间，这些命名空间的内容在不需要额外限定符的情况下就已处于作用域中。
在将标识符解析为特定名称时，Lean 会将当前命名空间和已打开的命名空间都考虑进去。尽管如此，
受保护的声明（即带有 `protected` 修饰器的声明）在其所处命名空间被打开时并不会被引入作用域。
至于标识符名称解析所使用的规则，当中那些会将当前命名空间和已开启的命名空间考虑进去的
在[“标识符作为项”]({{< relref "read-LeanRef-web-Chpt13.md" >}}#S13-1)一节中有详细描述。

{{< labelindex 
  type="例子" 
  summary="当前命名空间"
>}}
示范：`HotDrink`、`ColdDrink`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：当前命名空间" 
  open=false
>}}
归纳声明会创建一个新的命名空间，
其名称等同于归纳类型构造子的名称。
在下面的例子中，`HotDrink` 是一个归纳类型构造子，
它的归纳项构造子有 `coffee`、`tea` 和 `cocoa`：

```lean {wrapper=false, lineNos=false}
inductive HotDrink where
  | coffee
  | tea
  | cocoa
```

在命名空间外调用名称必须额外加上限定符，除非命名空间已被开启：

```lean {wrapper=false, lineNos=false}
#check HotDrink.tea
-- HotDrink.tea : HotDrink

#check tea
-- Unknown identifier `tea`

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

如果一个函数项是直接在 `HotDrink` 的命名空间中声明的，
那么函数体会在当前命名空间被设置为 `HotDrink` 的情况下被阐述。
此时项构造子都处于作用域中：

```lean {wrapper=false, lineNos=false}
def HotDrink.ofString? (s : String) := match s with
  | "coffee" => some coffee -- 这里能自动推断出是 HotDrink.coffee
  | "tea"    => some tea    -- 这里能自动推断出是 HotDrink.tea
  | "cocoa"  => some cocoa  -- 这里能自动推断出是 HotDrink.cocoa
  | _ => none
```

新的归纳声明又会创建一个新的命名空间：

```lean {wrapper=false, lineNos=false}
inductive ColdDrink where
  | water
  | juice
```

在 `HotDrink` 命名空间中声明 `HotDrink.toString` 可以不添加显式前缀；但要想
在 `HotDrink` 命名空间中声明 `ColdDrink.toString` 就必须提供显式的 `_root_` 限定符，
否则 `HotDrink.ColdDrink.toString` 就会被声明:

```lean {wrapper=false, lineNos=false}
namespace HotDrink

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

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

end HotDrink
```
{{< /admonition >}}

`open` 命令可用于开启一个命名空间，
使其内容在当前区段作用域中都是可用的。
此外还存在许多命名空间开启命令的变体，
它们为管理局部作用域提供了灵活性。

{{< labelindex 
  type="语法" 
  id_alias="单个命名空间开启"
>}}
`open …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
`open` 命令用于开启一个命名空间：

```lean {wrapper=false, lineNos=false}
command ::= ...
  | open openDecl
```
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="多个命名空间开启（递归）"
>}}
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
如果 `open` 后面跟的是一串标识符序列，
那么序列中的每个标识符都会作为命名空间被开启：

```lean {wrapper=false, lineNos=false}
openDecl ::= ...
  | ident ident*
```

每个命名空间的开启都是按照相对于当前命名空间进行处理的，
如此便会得到一个命名空间集合：当中的每个命名空间都会在
序列中的下一个命名空间被处理之前被开启。
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="多个命名空间的递归开启"
>}}
示范：`A`、`A.B`、`A.B.C`、`B`、`B.C`、`C`、`C.B`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：多个命名空间的递归开启" 
  open=false
>}}
命名空间的开启会按照相对于当前命名空间进行处理。
如果同一个组件出现在不同的命名空间路径中，
那么就可以用单个 `open` 命令来开启所有组件以便迭代地将每个命名空间引入作用域。
下述例子中的常量声明分散在不同的命名空间内：

```lean {wrapper=false, lineNos=false}
namespace A -- _root_.A
def a1 := "A.a1"
namespace B -- _root_.A.B
def a2 := "A.B.a2"
namespace C -- _root_.A.B.C
def a3 := "A.B.C.a3"
end C
end B
end A
namespace B -- _root_.B
def a4 := "B.a4"
namespace C -- _root_.B.C
def a5 := "B.C.a5"
end C
end B
namespace C -- _root_.C
def a6 := "C.a6"
namespace B -- _root_.C.B
def a7 := "C.B.a7"
end B
end C
```

当中的七个常量的值即为其完整路径名称。
前六个名称可以通过单个 `open` 命令一次性引入作用域，但
第七个不行：

```lean {wrapper=false, lineNos=false}
section
open A B C
example := [a1, a2, a3, a4, a5, a6, a7]
-- Unknown identifier `a7`
end
```

如果命令里出现的首个命名空间不是 `A` 而是 `A.B`，
那么 `_root_.A`、`_root_.B`、`_root_.B.C`、`_root_.C.B` 都不会被开启：

```lean {wrapper=false, lineNos=false}
section
open A.B C
example := [a1, a2, a3, a4, a5, a6]
end
-- Unknown identifier `a1`
-- Unknown identifier `a4`
-- Unknown identifier `a5`
```

开启 `A.B` 会使得 `_root_.A.B.C` 和 `_root_.C` 作为 `C` 可见。
如此后续开启的 `C` 实际上会将他们都开启。
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="单个命名空间开启（名称黑名单）"
>}}
`… hiding …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
带有 `hiding` 的 `open` 命令可以阻止一部分名称被引入作用域。
与递归开启一连串命名空间有所不同的是，
在这里只能指定单个待开启的命名空间。

```lean {wrapper=false, lineNos=false}
openDecl ::= ...
  | ident hiding ident ident*
```
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="单个命名空间开启（名称重命名）"
>}}
`… renaming (… → …),*`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
带有 `renaming` 的 `open` 命令可以允许一部分名称在待打开的命名空间中被重命名；
它们在当前区段作用域中可以通过新的名称来访问。与前者类似，
在这里同样也只能指定单个待开启的命名空间。

```lean {wrapper=false, lineNos=false}
openDecl ::= ...
  | ident renaming (ident → ident),*
```

ASCII 箭头（`->`）可用于替代 Unicode 箭头（`→`）。
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="单个命名空间开启（名称白名单）"
>}}
`… (…)`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
圆括号意味着只有那些位于圆括号之间的名称才会被引入作用域。

```lean {wrapper=false, lineNos=false}
openDecl ::= ...
  | ident (ident ident*)
```

被指定的命名空间会被添加到每个当前已开启的命名空间中，并且
每个名称都会在所有这些命名空间中被查找。
被列出的所有名称都必须是明确且唯一的；也就是说，
它们必须恰好仅存在于唯一一个被考虑的命名空间中。
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="单个命名空间开启（受限）"
>}}
`scoped …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
`scoped` 关键字意味着被指定的命名空间内的
受限属性、实例和语法都可被访问，但当中的
名称在作用域内却不可用。

```lean {wrapper=false, lineNos=false}
openDecl ::= ...
  | scoped ident ident*
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="单个命名空间内受限内容的访问"
>}}
示范：`NS`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：单个命名空间内受限内容的访问" 
  open=false
>}}
在下述例子中，
  一个受限的[记号](https://lean-lang.org/doc/reference/latest/Notations-and-Macros/Notations/#--tech-term-notation)以及
  一个常量声明
在命名空间 `NS` 中被创建：

```lean {wrapper=false, lineNos=false}
namespace NS
scoped notation "{!{" e "}!}" => (e, e)
def three := 3
end NS
```

该记号在命名空间外是无法使用的：

```lean {wrapper=false, lineNos=false}
def x := {!{ "pear" }!}
-- <example>:1:21-1:22: unexpected token '!'; expected '}'
```

但是 `open scoped` 命令使得该记号可用：

```lean {wrapper=false, lineNos=false}
open scoped NS
def x := {!{ "pear" }!}
```

然而名称 `NS.three` 却没被引入作用域。

```lean {wrapper=false, lineNos=false}
def y := three
-- Unknown identifier `three`
```
{{< /admonition >}}

## 6.1.2. 名称导出 Exporting Names {#S6-1-2}
{{< ctx level="3" >}}

**名称导出**使名称在当前命名空间中可用。与声明有所不同的是，
这个别名是完全透明的，名称调用会被直接解析到原始名称。
将名称导出到根部命名空间可以使其无需被限定即可被使用。
Lean 标准库就是这样做的：比如
  像 `Option` 的项构造子这样的名称，或者是
  如 `get` 这样的关键类型类方法。

{{< labelindex 
  type="语法" 
  id_alias="单个命名空间内的名称导出"
>}}
` export … (…)`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
`export` 命令可以将其他命名空间中的名称添加到当前命名空间中，
就好像它们是在当前命名空间中声明的一样。在当前命名空间被开启后，
这些被导出的名称也会被引入作用域。

```lean {wrapper=false, lineNos=false}
command ::= ...
  | export ident (ident*)
```

导出的名称在内部会被注册为它们目标的别名。
对于内核而言只有原始名称存在；
阐述器在将标识符解析为名称时会将别名解析为原始名称。
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="单个命名空间内的名称导出"
>}}
示范：`Veg`，`Leafy`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：单个命名空间内的名称导出" 
  open=false
>}}
归纳声明 `Veg.Leafy` 会创建归纳项构造子
`Veg.Leafy.spinach` 和 `Veg.Leafy.cabbage`：

```lean {wrapper=false, lineNos=false}
namespace Veg
inductive Leafy where
  | spinach
  | cabbage
export Leafy (spinach)
end Veg
export Veg.Leafy (cabbage)
```

第一个 `export` 命令使得 `Veg.Leafy.spinach` 可以作为 `Veg.spinach` 来访问，
因为当前命名空间是 `Veg`；
第二个 `export` 命令使得 `Veg.Leafy.cabbage` 可以作为 `cabbage` 来访问，
因为当前命名空间是根部命名空间。
{{< /admonition >}}

## 6.2. 区段作用域 Section Scopes {#S6-2}
{{< ctx level="2" >}}

许多命令的效果都是针对当前{{< labelindex 
  type="术语" 
  id_alias="区段作用域"
  title_alias="区段作用域 Section Scope"
>}}
{{< /labelindex >}}**区段作用域**（在语境明确时也可简称为“作用域”）的。
每个 Lean 模块都有一个区段作用域。
嵌套的作用域是由命令 `namespace` 或 `section` 以及命令组合器 `in` 所创建的。

下述内容在区段作用域内会被跟踪：

- {{< labelindex 
  type="术语" 
  id_alias="当前命名空间"
  title_alias="当前命名空间 The Current Namespace"
>}}
{{< /labelindex >}}**当前命名空间 The Current Namespace**

  当前命名空间即新声明将会位于的命名空间。此外[名称解析]({{< relref "read-LeanRef-web-Chpt13.md" >}}#术语-名称解析)会将当前命名空间的所有前缀包含在全局名称的作用域中。 

- {{< labelindex 
  type="术语" 
  id_alias="已开启的命名空间"
  title_alias="已开启的命名空间 Opened Namespace"
>}}
{{< /labelindex >}}**已开启的命名空间 Opened Namespace**

  一个命名空间若被开启，那么它所包含的名称在当前作用域中使用时就可以省略显式前缀。此外
  在已开启的命名空间中，受限属性和[受限语法扩展](https://lean-lang.org/doc/reference/latest/Notations-and-Macros/Defining-New-Syntax/#syntax-rules)在当前区段作用域中都是有效的。

- **编译器选项 Compiler Option**

  编译器选项如果有在区段作用域中被修改，
  那么在区段结束后就会被恢复为原先的值。

- **区段变量 Section Variable**

  [区段变量](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/#--tech-term-Section-variables)是那些会作为形参被自动添加进声明中的名称（或[实例隐式](https://lean-lang.org/doc/reference/latest/Type-Classes/#--tech-term-instance-implicit)形参）。
  当它们出现在定理的陈述中时，它们也会作为全称假设被自动添加进定理中。

### 6.2.1. 区段作用域的控制 Controlling Section Scopes {#S6-2-1}
{{< ctx level="3" >}}

`section` 命令
  会创建一个新的{{< labelindex 
  type="术语" 
  id_alias="区段"
  title_alias="区段 Section"
>}}
{{< /labelindex >}}**区段 Section** 作用域，但
  并不会修改当前命名空间、已开启的命名空间以及区段变量。
区段作用域中所做的更改会在区段结束后被复原。此外，
区段作用域还可能会
  将一组声明修饰器默认应用于区段中的所有声明。
区段作用域可以选择性地被命名；
关闭一个命名区段的 `end` 命令必须使用相同的名称。
如果区段名称有多个组件（即区段名称包含由 `.` 分隔的名称），
那么多个嵌套的区段作用域就会被引入。
区段名称没有其他效果，只是用于提高可读性而已。

{{< labelindex 
  type="语法" 
  id_alias="区段声明"
>}}
`section …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
`section` 命令会创建一个区段作用域，
该作用域会持续到 `end` 命令或文件结束为止。
区段声明的头部（如果存在的话）会对区段中的声明进行额外修改。

```lean {wrapper=false, lineNos=false}
command ::= ...
  | sectionHeader section ident?
```
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="区段声明（头部补充）"
>}}
`(@[expose])? public? noncomputable? meta? section …`
{{< /labelindex >}}
> [!info] 语法：{{< indexprint >}} 
>
> 如果区段声明的头部存在，那么它会对区段中的声明进行额外修改。
> 
> ```lean {wrapper=false, lineNos=false}
> sectionHeader ::= ...
>   | (@[expose])?
>     public? noncomputable? meta?
> ```
> 
> 如果头部包含 `noncomputable`，
> 那么区段中的所有声明
>   都会被视为非可计算的，并且
>   不会被生成对应的编译代码。
> 这对依赖于非计算推理原则（例如选择公理）的定义是必须的。
> 
> 其余的修饰器只在[模块](https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules/#--tech-term-module)中起效。
> 如果头部包含 `@[expose]`，
> 那么区段中的所有声明都会被[暴露](https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules/#--tech-term-exposed)。
> 如果头部包含 `public`，
> 那么此时的区段便是{{< labelindex 
  type="术语" 
  id_alias="公有区段"
  title_alias="公有区段 Public Section"
>}}
{{< /labelindex >}}公有区段，当中的声明默认都会是公有的而非私有的。
> 如果头部包含 `meta`，
> 那么区段中的声明都会被放置在[元阶段](https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules/#--tech-term-meta-phase)中。

{{< labelindex 
  type="例子" 
  summary="单个带有名称的区段的声明和关闭"
>}}
示范：`Greetings`，`Greetings.english`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：单个带有名称的区段的声明和关闭" 
  open=false
>}}
名称 `english` 在命名空间 `Greetings` 中被声明。

```lean {wrapper=false, lineNos=false}
def Greetings.english := "Hello"
```

`english` 在命名空间 `Greetings` 外无法被求值。

```lean {wrapper=false, lineNos=false}
#eval english
-- Unknown identifier `english`
```

开启一个区段可以将对全局作用域的修改限制在区段内。
这个区段被命名为 `Greetings`。

```lean {wrapper=false, lineNos=false}
section Greetings
```

尽管区段与声明所处的命名空间同名，
但是 `english` 也不会被引入作用域。
因为区段名称仅用于提高可读性和便于重构。

```lean {wrapper=false, lineNos=false}
#eval english
-- Unknown identifier `english`
```

开启命名空间 `Greetings` 
会将 `Greetings.english` 
作为 `english` 引入作用域：

```lean {wrapper=false, lineNos=false}
open Greetings
#eval english
-- "Hello"
```

要想关闭该区段就必须指明区段名称。

```lean {wrapper=false, lineNos=false}
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
```

在区段被关闭后，`open` 命令的效果就会被复原。

```lean {wrapper=false, lineNos=false}
#eval english
-- Unknown identifier `english`
```
{{< /admonition >}}

`namespace` 命令会创建一个新的区段作用域。在该区段作用域内，
  当前命名空间对应于命令中所指定的名称，并且
  该名称是相对于周围区段作用域中的当前命名空间来解释的。
在命名空间的作用域结束后，对区段作用域所做的更改都会被复原。这一点和区段一样。

要想关闭一个命名空间，需要向 `end` 命令提供当前命名空间的后缀，
该后缀会被移除。所有由引入该后缀的命名空间命令所引入的区段作用域都会被关闭。

{{< labelindex 
  type="语法" 
  id_alias="命名空间声明"
>}}
`namespace …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
`namespace` 命令通过将提供的标识符附加到当前命名空间来修改当前命名空间。
它会创建一个区段作用域，该作用域会持续到 `end` 命令或文件结束为止。

```lean {wrapper=false, lineNos=false}
command ::= ...
  | namespace ident
```
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="多个区段和多个命名空间的关闭"
>}}
`end`\
`end …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
没有标识符的 `end` 命令会关闭最近打开的区段。该区段必须是匿名的。

```lean {wrapper=false, lineNos=false}
command ::= ...
  | end
```

带有标识符的 `end` 命令会关闭最近打开的区段或命名空间；
如果要关闭的是区段，那么标识符必须是
自最近的 `namespace` 命令以来被开启的区段的名称的串联的后缀；
如果要关闭的是命名空间，那么标识符必须是
自最近的被开启的区段以来当前命名空间的扩展的后缀；
此后当前命名空间将会该后缀移除。

```lean {wrapper=false, lineNos=false}
command ::= ...
  | end ident
```
{{< /admonition >}}

用于关闭 `mutual` 块的 `end` 
是 `mutual` 语法的一部分，而
非 `end` 命令的一部分。

{{< labelindex 
  type="例子" 
  summary="多个和区段彼此嵌套的命名空间的关闭"
>}}
示范：`A.B.C`、`A`、`A.D.E`（位于 `A` 中的匿名 `section`）
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：多个和区段彼此嵌套的命名空间的关闭"
  open=false
>}}
命名空间和区段可以嵌套。
一个单独的 `end` 命令可以
  关闭一个或多个命名空间，或者
  关闭一个或多个区段，但是
  不能同时关闭两者。

在将当前命名空间通过两个 `namespace` 命令切换为 `A.B.C` 后，
`B.C` 便可以通过单个 `end` 命令被关闭：

```lean {wrapper=false, lineNos=false}
namespace A.B
namespace C
end B.C
```

此时当前命名空间就变成了 `A`。

紧接着一个匿名区段以及命名空间 `D.E` 被开启：

```lean {wrapper=false, lineNos=false}
section
namespace D.E
```

此时当前命名空间就变成了 `A.D.E`。
`end` 命令无法关闭他们仨，因为中间有一个区段：

```lean {wrapper=false, lineNos=false}
end A.D.E
-- Invalid name after `end`: Expected `D.E`, but found `A.D.E`
```

此时我们必须使用多次 `end` 命令来将其关闭。

```lean {wrapper=false, lineNos=false}
end D.E
end
end A
```
{{< /admonition >}}

与使用单个命令开启一个区段相比，
`in` 组合子可以创建仅用于单个命令的区段作用域。
`in` 组合子是右结合的，允许将多个对作用域做出的修改进行堆叠。

{{< labelindex 
  type="语法" 
  id_alias="区段作用域的局部开启"
>}}
`in …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
`in` 命令组合器会为单个命令创建一个区段作用域。

```lean {wrapper=false, lineNos=false}
command ::= ...
  | command in
    command
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="单个命名空间仅为单条命令开启"
>}}
示范：`Dessert.cupcake`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：单个命名空间仅为单条命令开启" 
  open=false
>}}
我们可以通过 `in` 来使得命名空间的内容只为单个命令可见。

```lean {wrapper=false, lineNos=false}
def Dessert.cupcake := "delicious"

open Dessert in
#eval cupcake
```

`open` 的效果在该命令之后就被复原了。

```lean {wrapper=false, lineNos=false}
#eval cupcake
-- Unknown identifier `cupcake`
```
{{< /admonition >}}

### 6.2.2. 区段变量 Section Variables {#S6-2-2}
{{< ctx level="3" >}}

{{< labelindex 
  type="术语" 
  id_alias="区段变量"
  title_alias="区段变量 Section Variable"
>}}
{{< /labelindex >}}**区段变量 Section Variable** 会作为形参被自动添加进那些引用它们的声明中。无论 `autoImplicit` 选项是否为 `true`，这个过程都会发生。
区段变量可能是
  隐式的、
  严格隐式的、或者是
  显式的；
  实例隐式的区段变量会被特殊处理。

当一个区段变量的名称出现在非定理声明中时，它就会作为形参被添加进声明中。
任何引用该变量的实例隐式区段变量也会被添加进声明中；同样，
如果被添加的变量依赖于其他变量，
那么这些变量也会被添加进声明中。
这个过程会被不断迭代，直至没有剩余的依赖关系。
所有区段变量都会按照它们被声明的顺序被依次添加进声明中，
并且添加会发生在所有其他形参之前。
至于定理声明，只有当出现在定理的陈述中时，区段变量才会被添加进定理中；不然的话
如果证明项用到了区段变量，那么修改定理的证明就可能导致定理陈述发生改变。

区段变量在常量声明主体被阐述之前是不会作为声明的形参被添加进声明当中的。这意味着
  它们在递归声明中不可以发生变化，并且
  它们的值是固定的。
显式形参
  可以遮蔽区段变量，并且
  可以用在那些值必须发生变化的声明中。

区段变量是通过 `variable` 命令来声明的。

{{< labelindex 
  type="语法" 
  id_alias="多个区段变量声明"
>}}
`variable …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
```lean {wrapper=false, lineNos=false}
command ::= ...
  | variable bracketedBinder bracketedBinder*
```

其中括号绑定器的语法与[常量声明头部的语法]({{< relref "read-LeanRef-web-Chpt07.md" >}}#S7-2-3)相同。
{{< /admonition >}}


{{< labelindex 
  type="例子" 
  summary="多个区段变量的声明和调用"
>}}
示范：`addAll`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：多个区段变量的声明和调用" 
  open=false
>}}
尽管隐式形参自动声明功能在下述区段中被禁用；
但是仍然有一些区段变量被声明了。

```lean {wrapper=false, lineNos=false}
section
set_option autoImplicit false
universe u
variable {α : Type u} (xs : List α) [Zero α] [Add α]
```

由于隐式形参自动声明功能被禁用，并且 
`β` 既不是区段变量也没有作为函数的形参被声明，
因此下述常量声明会报错：

```lean {wrapper=false, lineNos=false}
def addAll (lst : List β) : β :=
  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` 甚至不需要在定义中直接写出，
因为它使用了区段变量：

```lean {wrapper=false, lineNos=false}
def addAll :=
  xs.foldr (init := 0) (· + ·)
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="某些区段变量可能无法用于递归函数声明"
>}}
示范：`copies`，`length`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：某些区段变量可能无法用于递归函数声明" 
  open=false
>}}
区段变量在递归函数中是固定的。
变量 `length` 代表一个逐步递减的自然数：

```lean {wrapper=false, lineNos=false}
variable (length : Nat)
```

但是其无法被直接用于递归函数的声明，
因为函数主体并未将区段变量视为形参：

```lean {wrapper=false, lineNos=false}
def copies (x : α) : List α :=
  match length with
  | 0 => []
  | length' + 1 => x :: copies length' x
```

报错的原因是 `copies` 只期望单个显式实参，但却收到了两个：

```lean {wrapper=false, lineNos=false}
-- Function expected at
--   copies length'
-- but this term has type
--   List Nat
-- Note: Expected a function because 
-- this term is being applied to the argument
--   x
```

不过我们可以用显式形参来遮蔽区段变量 `length`，
从而使其可以被用于递归函数的声明：

```lean {wrapper=false, lineNos=false}
def copies (length : Nat) (x : α) : List α :=
  match length with
  | 0 => []
  | length' + 1 => x :: copies length' x
```
{{< /admonition >}}

要想将一个区段变量添加到定理中（即便它没有在定理陈述中被显式提及），
就可以用 `include` 命令标记该区段变量：
所有被 `include` 标记的变量都会被添加到定理陈述当中。 
`omit` 命令则用于移除变量的 `include` 标记。
通常建议在定理中使用 `omit` 来移除不必要的变量。

{{< labelindex 
  type="例子" 
  summary="多个区段变量的添加和移除"
>}}
示范：`p`、`pZero`、`pStep`、`pFifteen`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：多个区段变量的添加和移除" 
  open=false
>}}
下述区段中的变量包括
  一个谓词 `p`，以及
  两个有助于证明 `∀ n, p n` 的假设，外加
  一个无用的额外假设 `pFifteen`：

```lean {wrapper=false, lineNos=false}
section
variable {p : Nat → Prop}
variable (pZero : p 0) (pStep : ∀ n, p n → p (n + 1))
variable (pFifteen : p 15)
```

但在这里只有 `p` 被添加到该定理的假设中，
所以该定理无法被证明。

```lean {wrapper=false, lineNos=false}
theorem p_all : ∀ n, p n := by
  intro n
  induction n
-- unsolved goals
```

而下述代码中 `include` 命令会无条件地将额外的假设添加进来：
此时由于无用的假设 `pFifteen` 被插入了，Lean 会发出警告：

```lean {wrapper=false, lineNos=false}
include pZero pStep pFifteen

theorem p_all : ∀ n, p n := by
  intro n
  induction n <;> simp [*]
-- 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`
```

要避免这种情况，可以通过 `omit` 来移除多余的假设 `pFifteen`：

```lean {wrapper=false, lineNos=false}
include pZero pStep pFifteen

omit pFifteen in
theorem p_all : ∀ n, p n := by
  intro n
  induction n <;> simp [*]
end
```
{{< /admonition >}}

## 索引 Index {#index}

### 术语

{{< indexlist type="术语" sort="title" >}}

### 语法

{{< indexlist type="语法" >}}

### 常量

{{< indexlist type="常量" code_wrap=true >}}

### 定理

{{< indexlist type="定理" code_wrap=true >}}

### 公理

{{< indexlist type="公理" code_wrap=true >}}

### 归纳

{{< indexlist type="归纳" code_wrap=true >}}

### 结构

{{< indexlist type="结构" code_wrap=true >}}

### 类型类

{{< indexlist type="类型类" code_wrap=true >}}

### 选项

{{< indexlist type="选项" code_wrap=true >}}

### 属性

{{< indexlist type="属性" code_wrap=true >}}

### 例子

{{< indexlist type="例子" print_section=false >}}


---

> 作者: [沉积岩](ych817.github.io)  
> URL: https://ych817.github.io/posts/2c6ec0d/