# 翻译-Lean Language Reference-07-常量声明

{{< ctxset prefix="7" >}}
{{< 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 中用于名称定义：

- `def`

- `abbrev`

- `example`

- `theorem`

- `opaque`

上述所有命令会根据签名对一个项进行展开。
除了 `example` 命令会丢弃结果以外，
其他命令都会将 Lean 核心语言中的结果表达式保存到环境中以供将来使用。
`instance` 命令的用法在[实例声明](https://lean-lang.org/doc/reference/latest/Type-Classes/Instance-Declarations/#instance-declarations)一节中会详细介绍。

## 7.1. 声明修饰器 Modifiers {#S7-1}
{{< ctx level="2" >}}

常量声明可以接收一连串的{{< labelindex 
  type="术语" 
  id_alias="常量声明修饰器"
  title_alias="常量声明修饰器 Modifier"
/>}}**声明修饰器 Modifier**，这些修饰器都是可选的。
修饰器会改变常量声明的某些解释。例如：
  它们可以为常量添加文档注释，或者是
  改变常量的作用域。
修饰器的顺序是固定的，
但并非所有声明都可以接纳每种修饰器。

{{< labelindex 
  type="语法" 
  id_alias="常量声明（修饰补充）"
>}}
`… noncomputable? unsafe? (partial | nonrec)?`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
声明修饰器按顺序包含下述组成部分。这些组成部分都是可选的：

- 文档注释，

- 一连串[属性](https://lean-lang.org/doc/reference/latest/Attributes/#--tech-term-Attributes)，

- 命名空间控制——待声明名称究竟是私有的（`private`）还是受保护的（`protected`），

- `noncomputable` 关键字——使得定义免于编译，

- `unsafe` 关键字，以及

- 一个递归修饰器 `partial` 或者 `nonrec` ——前者用于禁用可以停机性证明，后者用于完全禁止递归。

```lean {wrapper=false, lineNos=false}
declModifiers ::=
  docComment?
  attributes?
  visibility?
  noncomputable?
  unsafe?
  (partial | nonrec)?
```
{{< /admonition >}}

{{< labelindex 
  type="术语" 
  id_alias="常量声明文档注释"
  title_alias="常量声明文档注释 Documentation Comment"
/>}}**文档注释 Documentation Comment** 用于为其所修饰的声明提供源码内 API 文档。
文档注释其实不是普通注释：
如果将文档注释放在无法作为文档被处理的位置，
那么就会引发语法错误。此外在某些
需要提供文本内容但是使用字符串转义又会过于繁琐的地方
也可以使用文档注释——比如
`#guard_msgs` 命令所期望的消息内容，

{{< labelindex 
  type="语法" 
  id_alias="常量声明（文档注释修饰补充）"
>}}
`\-- … -\`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
文档注释就像普通的块注释一样，
它们都以 `-/` 结尾，但是
它们文档注释以 `/--` 而非 `/-` 开头。

```lean {wrapper=false, lineNos=false}
docComment ::=
  /--
  ...
  -/
```
{{< /admonition >}}

属性是一个可扩展的修饰器集合，用于将额外的信息与声明关联起来。
关于属性的详细说明请参见[专门的章节](https://lean-lang.org/doc/reference/latest/Attributes/#attributes)。

如果一个声明被标记为 `private`，
那么对应的名称在声明所处模块之外是无法被访问的。
如果一个声明被标记为 `protected`，
那么即便其命名空间被打开也不会将其引入到作用域中。

被 `noncomputable` 修饰的函数
  不会被编译，也
  无法被执行。
满足以下情况的函数肯定是不可计算的：
  如果它们使用了不可计算的推理原则来产生与其返回结果相关的数据——比如
    选择公理
    排中律，或者是
  如果它们使用了 Lean 中的某些特性，
    这些特性为了效率原因而被排除在代码生成之外，
    比如归纳项的递归子。
即便不可计算函数无法被编译和执行，
他们在规范和推理中依然非常有用。

尽管不可计算函数无法被编译和执行，
但是在规约 Specification 和推理中它们却非常有用，

`unsafe` 标记可以使
  声明免于内核检查，并且允许它
  访问那些可能破坏 Lean 安全性保证的特性。
使用 `unsafe` 标记
  必须非常小心谨慎，并且
  最好确保自己对 Lean 内部机制有透彻的理解。

## 7.2. 头部、类型签名 Headers and Signatures {#S7-2}
{{< ctx level="2" >}}

常量声明的{{< labelindex 
  type="术语" 
  id_alias="常量声明头部"
  title_alias="常量声明头部 Header"
/>}}**头部 Header** 包含了
  待声明的常量名称，如果可能的话
  还会附带其类型签名。
常量的{{< labelindex 
  type="术语" 
  id_alias="常量的类型签名"
  title_alias="常量的类型签名 Signature"
/>}}**类型签名 Signature** 指定了常量的使用方式。
类型签名中所包含的信息不仅只有
  类型本身，还包括诸如
  [宇宙层级形参]({{< relref "read-LeanRef-web-Chpt04.md" >}}#术语-宇宙层级形参)以及
  可选形参的默认值等信息。
在 Lean 中，
类型签名在不同种类的常量声明里
都是以一致的格式书写的。

### 7.2.1. 常量名称 Declaration Names {#S7-2-1}
{{< ctx level="3" >}}

大部分常量声明的头部都以**待声明的常量名称**开头，
名称后可能还跟着与之对应的类型签名——即
常量的形参和函数返回类型。
待声明名称包含一个标识符，其后
可能还尾随一个或多个宇宙层级形参。

{{< labelindex 
  type="语法" 
  id_alias="常量声明（常量命名）"
>}}
`….{…, …}`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
没有宇宙层级形参的待声明常量名称只包含一个标识符：

```lean {wrapper=false, lineNos=false}
declId ::=
    ident
```

具有宇宙层级形参的待声明常量名称包含一个标识符，后面
跟着一个点号以及包裹在花括号内的一或多个宇宙层级形参：

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

这些宇宙层级名称都是绑定出现。
{{< /admonition >}}

`example` 不包含待声明名称；此外对[实例声明](https://lean-lang.org/doc/reference/latest/Type-Classes/Instance-Declarations/#instance-declarations)而言待声明名称是可选的。

### 7.2.2. 类型签名 Parameters and Types {#S7-2-2}
{{< ctx level="3" >}}
在待声明名称之后可能会出现类型签名。
类型签名指定了
  待声明常量的形参以及
  函数返回类型。

{{< labelindex 
  type="语法" 
  id_alias="常量声明（形参声明、返回结果类型注解补充）"
>}}
`… : …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
类型签名包含
  零个或多个形参，
  后面跟着一个冒号外加返回结果的类型。

```lean {wrapper=false, lineNos=false}
declSig ::=
    (ident | hole | bracketedBinder)* : term
```
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="常量声明（形参声明、返回结果类型注解省略）"
>}}
`… (: …)?`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
类型签名里返回结果的类型注解通常是可选的。
我们可以只提供形参而省略返回结果类型。

```lean {wrapper=false, lineNos=false}
optDeclSig ::=
    (ident | hole | bracketedBinder)* (: term)?
```
{{< /admonition >}}

形参可以是以下三种形式中的任意一种：

- 一个标识符 `ident`，被用于命名一个形参，但并不提供类型信息。
  这些形参的类型推导必须在阐述中完成。

- 一个下划线 `_`，用于指代一个在局部作用域中无法通过名称访问的形参。
  这些形参的类型推导也必须在阐述中完成。

- 一个括号绑定器 `bracketedBinder`，其可以指定一个或多个形参的各个方面，包括它们的
    名称、类型、默认值，以及它们是否为
      显式的、
      隐式的、
      严格隐式的、
      实例隐式的。

### 7.2.3. 括号绑定器 Bracketed Parameter Bindings {#S7-2-3}
{{< ctx level="3" >}}

非标识符且非下划线的形参统称为{{< labelindex 
  type="术语" 
  id_alias="常量声明括号绑定器"
  title_alias="常量声明括号绑定器 Bracketed Binder"
/>}}**括号绑定器 Bracketed Binder**，
因为它们的每一种语法形式都含有方括号、花括号或圆括号。
所有括号绑定器都指定了形参的类型，
并且大多数都会包含形参的名称。
那些使用下划线 (`_`) 代替名称的形参则是匿名形参。

{{< labelindex 
  type="语法" 
  id_alias="常量声明（显式形参声明类型注解补充）"
>}}
`(… … : …)`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
带圆括号的形参声明会指定一个显式形参：
如果圆括号内提供了多个标识符或下划线，
那么它们都会成为显式形参，且具有相同的类型。

```lean {wrapper=false, lineNos=false}
bracketedBinder ::=
    ((ident | hole) (ident | hole)* : term)
```
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="常量声明（可选、自动形参声明类型注解补充）"
>}}
`(… … : … := …)`
{{< /labelindex >}}
> [!info] 语法：{{< indexprint >}}
> 包裹在括号内的形参外加一个 `:=` 就可以为形参指定一个默认值。
> 带默认值的形参被称为{{< labelindex 
  type="术语" 
  id_alias="函数项的可选形参"
  title_alias="函数项的可选形参 Optional Parameter"
/>}}**可选形参 Optional Parameter**。
> 如果在调用处没有提供该形参，那么默认值就会被使用。
> 在类型签名中，
> 位于其前面的形参对于默认值而言是可见的，
> 因此这些形参在调用处的实际值会被代换到默认值中。
> 
> 如果一个策略脚本被提供，
> 那么这些策略会在调用处被执行以合成出一个实参的值。
> 需要借助策略合成对应实参的形参称为
{{< labelindex 
  type="术语" 
  id_alias="函数项的自动形参"
  title_alias="函数项的自动形参 Automatic Parameter"
/>}}
> **自动形参 Automatic Parameter**。
> 
> ```lean {wrapper=false, lineNos=false}
> bracketedBinder ::= ...
>   | ((ident | hole) (ident | hole)* : term := term)
> ```

{{< labelindex 
  type="语法" 
  id_alias="常量声明（普通隐式形参声明类型注解补充）"
>}}
`{… … : …}`
{{< /labelindex >}}
> [!info] 语法：{{< indexprint >}}
> 包裹在花括号中的形参被称为[**普通隐式形参 Ordinary Implicit Parameter**]({{< relref "read-LeanRef-web-Chpt13.md" >}}#术语-函数项的普通隐式形参)。
> 除非是在常量调用处使用具名方式提供了对应的实参，
> 否则实参会在常量调用处通过合一来合成。
> 隐式形参会在所有常量调用处被合成。
> 
> ```lean {wrapper=false, lineNos=false}
> bracketedBinder ::= ...
>   | {(ident | hole) (ident | hole)* : term}
> ```

{{< labelindex 
  type="语法" 
  id_alias="常量声明（严格隐式形参声明类型注解补充）"
>}}
`⦃… … : …⦄`\
`{{… … : …}}`
{{< /labelindex >}}
> [!info] 语法：{{< indexprint >}}
> 包裹在双花括号中的形参被称为[**严格隐式形参 Strict Implicit Parameter**]({{< relref "read-LeanRef-web-Chpt13.md" >}}#术语-函数项的严格隐式形参)。
> `⦃ … ⦄` 和 `{{ … }}` 的效果是一样的。正如普通隐式形参，
> 如果严格隐式形参在常量调用处没有使用具名方式提供对应的实参，
> 那么就会在常量调用处通过合一来合成。严格隐式形参的对应实参
> 只有在签名中后续的形参也被提供实参时才会在常量调用处被合成。
> 
> ```lean {wrapper=false, lineNos=false}
> bracketedBinder ::= ...
>   | ⦃(ident | hole) (ident | hole)* : term⦄
> 
> bracketedBinder ::= ...
>   | {{(ident | hole) (ident | hole)* : term}}
> ```


{{< labelindex 
  type="语法" 
  id_alias="常量声明（实例隐式形参声明类型注解补充）"
>}}
`[(… :)? …]`
{{< /labelindex >}}
> [!info] 语法：{{< indexprint >}}
> 
> 方括号内的形参将指定[**实例隐式形参 Instance Implicit Parameter**](https://lean-lang.org/doc/reference/latest/Type-Classes/#--tech-term-instance-implicit)，
> 后者用于在常量调用处通过[实例合成](https://lean-lang.org/doc/reference/latest/Type-Classes/#--tech-term-synthesizes)来合成对应的实参。
> 
> ```lean {wrapper=false, lineNos=false}
> bracketedBinder ::= ...
>   | [(ident :)? term]
> ```

形参始终处于冒号后的返回结果类型注解表达式的作用域内，
它们同样也处于声明主体表达式的作用域内；与之相对的是，
仅在返回结果类型注解表达式中绑定的名称只在该区域内有效。
可见形参的名称实际上被使用了两次，分别

- 作为返回结果类型注解表达式中的名称——
  作为依赖函数类型的一部分被绑定；

- 作为声明主体表达式中的名称——
  它们被一个 `fun` 所绑定。

{{< labelindex 
  type="例子" 
  summary="括号绑定器里声明的形参的作用域最大"
>}}
示范：`Nat.add`、`mustBeEqual`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：括号绑定器里声明的形参的作用域最大" 
  open=false
>}}
`add` 的类型签名中包含了两个形参 `n` 和 `k`。注意到
返回结果的类型是一个函数类型 `(k : Nat) → Nat`，其中包含了 `k`。
形参 `n` 是处于声明主体表达式作用域内的，而 `k` 并不在作用域内。

```lean {wrapper=false, lineNos=false}
def add (n : Nat) : (k : Nat) → Nat
  | 0 => n
  | k' + 1 => 1 + add n k'
```

正如 `add` 一样，`mustBeEqual` 的签名中也包含了一个形参 `n`。
它既处于返回结果类型注解表达式的作用域内，因为它出现在一个命题当中；
它又处于声明主体表达式的作用域内，因为它作为消息的一部分出现。

```lean {wrapper=false, lineNos=false}
def mustBeEqual (n : Nat) : (k : Nat) → n = k → String :=
  fun _ =>
    fun
    | rfl => s!"Equal - both are {n}!"
```
{{< /admonition >}}

[函数项应用]({{< relref "read-LeanRef-web-Chpt13.md" >}}#S13-4)相关章节内有
  [可选](#术语-函数项的可选形参)、
  [自动](#术语-函数项的自动形参)、
  [隐式]({{< relref "read-LeanRef-web-Chpt13.md" >}}#术语-函数项的普通隐式形参)以及
  [实例隐式](https://lean-lang.org/doc/reference/latest/Type-Classes/#--tech-term-instance-implicit)
形参的详细说明。

### 7.2.4. 自动声明的隐式形参 Automatic Implicit Parameters {#S7-2-4}
{{< ctx level="3" >}}

类型签名中出现的其他未绑定名称在默认情况下可能会被自动转换为隐式形参。
这些行为被称作是{{< labelindex 
  type="术语" 
  id_alias="函数项的隐式形参的自动声明"
  title_alias="函数项的隐式形参的自动声明 Automatic Declaration of Implicit Parameter"
/>}}
**隐式形参的自动声明 Automatic Declaration of Implicit Parameter**。
这种情况会在下述情况中发生：
  形参不是正在被应用的函数，并且
  形参的类型以及它们的任何顺序约束
  在类型签名中都有充足的信息来推断。
这个过程是迭代的：
如果新插入隐式形参的类型推断包含了无法被唯一确定的依赖项，
那么这些依赖项将进一步被替换为隐式形参。

至于那些无法与类型签名中写出的名称对应上的的隐式形参，
它们将会被自动赋予类似于证明中无法访问的假设的名称，
这些名称无法被访问。在类型签名中它们会被加上一个匕首符号 (`✝`) 。
这可以防止 Lean 随意选择的名称成为 API 的一部分，
从而被用作具名参数。

{{< labelindex 
  type="例子" 
  summary="类型签名里未绑定名称的自动绑定"
>}}
示范：`List.map`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类型签名里未绑定名称的自动绑定" 
  open=false
>}}
在下述 `map` 的声明中，`α`、`β` 并没有被显式绑定。
这并没有导致报错，相反它们被转换为隐式形参。
由于它们必须是类型，但又没有任何约束来限制它们的宇宙，
因此会进一步插入宇宙层级形参 `u` 和 `v`。

```lean {wrapper=false, lineNos=false}
set_option autoImplicit true

def map (f : α → β) : (xs : List α) → List β
  | [] => []
  | x :: xs => f x :: map f xs
```

`map` 的完整类型签名如下：

```lean {wrapper=false, lineNos=false}
#check List.map
-- List.map.{u_1, u_2} {α : Type u_1} {β : Type u_2} 
--   (f : α → β) (l : List α) : 
--   List β
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="类型签名里未出现的宇宙层级名称的自动绑定"
>}}
示范：`List.map`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类型签名里未出现的宇宙层级名称的自动绑定" 
  open=false
>}}
下述例子会产生报错，`α` 和 `β` 并没有被显式绑定；
这是因为选项 `autoImplicit` 被设置为 `false` 所导致的：

```lean {wrapper=false, lineNos=false}
set_option autoImplicit false

def map (f : α → β) : (xs : List α) → List β
  | [] => []
  | x :: xs => f x :: map f xs
-- 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`.
```

完整的类型签名可以使得常量声明得以被接受：

```lean {wrapper=false, lineNos=false}
set_option autoImplicit false

def map.{u, v} {α : Type u} {β : Type v}
    (f : α → β) :
    (xs : List α) → List β
  | [] => []
  | x :: xs => f x :: map f xs
```

Lean 会为没有类型注解的类型形参自动插入宇宙层级形参。
类型形参的宇宙层级可以被推断出来，并且
即便 `autoImplicit` 被禁用，
也会自动插入适当的宇宙层级形参：

```lean {wrapper=false, lineNos=false}
set_option autoImplicit false

def map {α β} (f : α → β) :
    (xs : List α) → List β
  | [] => []
  | x :: xs => f x :: map f xs
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="类型签名里未出现名称的自动绑定"
>}}
示范：`AtLeast`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类型签名里未出现名称的自动绑定" 
  open=false
>}}
给定
  一个类型为 `Fin n`（即自身大小不超过 `n`）的数，以及
  一个类型为 `AtLeast i`（附带自身不小于 `i` 的证明）的数：

```lean {wrapper=false, lineNos=false}
set_option autoImplicit true
structure AtLeast (i : Fin n) where
  val : Nat
  val_gt_i : val ≥ i.val
```

这些数字可以被相加：

```lean {wrapper=false, lineNos=false}
def AtLeast.add (x y : AtLeast i) : AtLeast i :=
  AtLeast.mk (x.val + y.val) <| by
    cases x
    cases y
    dsimp only
    omega
```

`AtLeast.add` 的签名需要多次隐式形参自动声明。
首先 `i` 会被插入，但是 `i` 的类型依赖于 `Fin n` 的上界 `n`；
接着 `n` 会被插入，并且名称由机器选择。
由于 `n` 的类型是 `Nat`，它没有任何依赖，因此该过程会终止。
最终的类型签名可以通过 `#check` 来查看：

```lean {wrapper=false, lineNos=false}
#check AtLeast.add
-- AtLeast.add {n✝ : Nat} {i : Fin n✝} 
-- (x y : AtLeast i) : AtLeast i
```
{{< /admonition >}}

隐式形参自动声明会在
由区段变量声明所导致的形参插入之后发生。
区段变量所对应的形参具有与对应变量相同的名称，即便
它们无法与类型签名中直接写出的名称对应上，并且
禁用隐式形参自动声明也不会影响那些对应于区段变量的形参；
然而在隐式形参自动声明功能被启用时，
那些包含其他原本未受绑定的变量的区段变量声明会接收额外的区段变量，
这些区段变量遵循与隐式形参相同的规则。

隐式形参自动声明是由两个选项控制的；
默认情况下隐式形参自动声明是宽松的，
这意味着任何未绑定的标识符都可能成为自动插入的候选项。
将 `relaxedAutoImplicit` 选项设置为 `false` 会
  禁用宽松模式，并且在选择自动插入的候选项时
  只会考虑那些由单个字符后跟零个或多个数字组成的标识符。

{{< labelindex 
  type="选项" 
  id_alias="relaxedAutoImplicit"
  summary="默认为 `true`"
>}}
是否允许非空原子标识符被自动声明为隐式形参
{{< /labelindex >}}
{{< admonition 
  type=info
  title="选项：`{{< indexprint >}}`" 
>}}
默认值：`true`。

在“宽松”模式启用时，任何非空原子标识符
都可以作为自动声明的隐式形参的候选项
（参见选项 [`autoImplicit`](#选项-autoImplicit)）。
{{< /admonition >}}

{{< labelindex 
  type="选项" 
  id_alias="autoImplicit"
  summary="默认为 `true`"
>}}
是否将声明头部中的局部未绑定名称自动声明为隐式形参
{{< /labelindex >}}
{{< admonition 
  type=info
  title="选项：`{{< indexprint >}}`" 
>}}
默认值：`true`。

声明头部中的局部未绑定名称会被自动声明为隐式形参。
在（默认启用的）“宽松”模式下，任何原子标识符都可以作为候选项，
否则的话只有由单个字符后跟数字组成的标识符才能作为候选项。
比如头部 `def f (x : Vector α n) : Vector α n :=`
就会自动声明隐式形参 `{α n}`。
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="隐式形参自动声明在（非）宽松模式下的表现"
>}}
示范：`Answer`、`select`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：隐式形参自动声明在（非）宽松模式下的表现" 
  open=false
>}}
错误拼写的标识符或者是缺失的导入
可能会声明不想要的隐式形参，比如：

```lean {wrapper=false, lineNos=false}
set_option autoImplicit true
set_option relaxedAutoImplicit true

inductive Answer where
  | yes
  | maybe
  | no

def select (choices : α × α × α) : Asnwer →  α -- Asnwer 这里有问题
  | .yes => choices.1
  | .maybe => choices.2.1
  | .no => choices.2.2
-- Invalid dotted identifier notation: 
-- The expected type of `.yes`
--   Asnwer
-- is not of the form `C ...` or `... → C ...` 
-- where C is a constant
```

上述报错信息意味着
实参的类型不是一个常量，
因此无法在模式中使用点号表示法。
这是因为其类型签名变成如下形式：

```lean {wrapper=false, lineNos=false}
select.{u_1, u_2}
  {α : Type u_1}
  {Asnwer : Sort u_2}
  (choices : α × α × α) :
  Asnwer → α
```

禁用 `relaxedAutoImplicit` 选项
可以使报错信息更加清晰，同时仍然
允许类型被自动插入：

```lean {wrapper=false, lineNos=false}
set_option autoImplicit true
set_option relaxedAutoImplicit false

def select (choices : α × α × α) : Asnwer →  α -- Asnwer 这里有问题
  | .yes => choices.1
  | .maybe => choices.2.1
  | .no => choices.2.2
-- Unknown identifier `Asnwer`
-- 
-- Note: It is not possible to treat `Asnwer` as an implicitly bound variable here 
-- because it has multiple characters while the `relaxedAutoImplicit` option 
-- is set to `false`.
```

修正拼写错误可以使得定义被接受：

```lean {wrapper=false, lineNos=false}
set_option autoImplicit true
set_option relaxedAutoImplicit false

def select (choices : α × α × α) : Answer →  α
  | .yes => choices.1
  | .maybe => choices.2.1
  | .no => choices.2.2
```

禁用 `autoImplicit` 选项会导致无法自动插入隐式形参：

```lean {wrapper=false, lineNos=false}
set_option autoImplicit false
set_option relaxedAutoImplicit false

def select (choices : α × α × α) : Answer →  α -- 四个 α 有问题
  | .yes => choices.1
  | .maybe => choices.2.1
  | .no => choices.2.2
-- Unknown identifier `α`
-- 
-- Note: It is not possible to treat `α` as an implicitly bound variable here 
-- because the `autoImplicit` option is set to `false`.
```
{{< /admonition >}}

## 7.3. 常量声明 Definitions {#S7-3}
{{< ctx level="2" >}}
常量声明会将一个新的常量添加到全局环境中，该常量的名称对应于一个项。
作为 Lean 核心语言中定义等价性的一部分，这个新的常量可以通过
[δ 归约]({{< relref "read-LeanRef-web-Chpt04.md" >}}#术语-项的δ归约)
展开为它所对应的定义。在阐述器中，这种替换是由常量的[可归约性](#术语-可归约性)所控制的。
新的常量可以是宇宙多态的，在这种情况下，
每个实例都可以通过不同的宇宙层级参数来实例化它。

函数常量声明可以是递归的。为了保持 Lean 类型理论
作为逻辑的一致性，递归函数要么
  得对内核不透明（比如将它们声明为 [`partial`](#S7-6-6-1)），要么就
  得被证明满足可以停机性（证明需要用到[递归定义一节](#S7-6)中介绍的策略）。

常量声明的头部和主体会一起被阐述。
如果头部没有被完整地指定（比如缺少了形参类型或者是缺少了返回结果类型），
那么主体可能会提供足够的信息使得阐述器可以重建缺失的部分。然而，
[实例隐式形参](https://lean-lang.org/doc/reference/latest/Type-Classes/#--tech-term-instance-implicit)的指定必须在头部或者是作为[区段变量]({{< relref "read-LeanRef-web-Chpt06.md" >}}#术语-区段变量)完成。

{{< labelindex 
  type="语法" 
  id_alias="常量声明"
>}}
`… def … := …`\
`… def … (| … => …)*`\
`… def … where …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
那些使用 `:=` 的常量声明会将右侧的项与常量名称关联起来。
  每多出一个形参，这个项就会被多裹进一层 `fun`；
  而其类型则是通过在函数类型中绑定这些形参来确定。
使用 `def` 的常量声明都是[半归约的](https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/#--tech-term-Semireducible)。

```lean {wrapper=false, lineNos=false}
command ::= ...
  | declModifiers
    def declId optDeclSig := term
```

常量声明也可以使用模式匹配的方式书写。
这些声明会被脱糖为使用 `match` 的形式。

```lean {wrapper=false, lineNos=false}
command ::= ...
  | declModifiers
    def declId optDeclSig
      (| term => term)*
```

结构类型下的值，或者是返回结构值的函数，
可以通过在 `where` 之后为它们的字段提供具体的值来定义：

```lean {wrapper=false, lineNos=false}
command ::= ...
  | declModifiers
    def declId optDeclSig where
      structInstField*
```

在[模块](https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules/#--tech-term-module)中，使用 `def` 的常量声明的主体默认情况下不会被暴露。
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="缩写声明"
>}}
`… abbrev … := …`\
`… abbrev … (| … => …)*`\
`… abbrev … where …`
{{< /labelindex >}}
> [!info] 语法：{{< indexprint >}}
> {{< labelindex 
  type="术语" 
  id_alias="缩写"
  title_alias="缩写 Abbreviation"
>}}
{{< /labelindex >}}**缩写 Abbreviation** 声明与使用 `def` 的常量声明类似，
> 只不过它们是[可归约的](https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/#--tech-term-Reducible)。
> 
> ```lean {wrapper=false, lineNos=false}
> command ::= ...
>   | declModifiers
>     abbrev declId optDeclSig := term
> 
> command ::= ...
>   | declModifiers
>     abbrev declId optDeclSig
>       (| term => term)*
> 
> command ::= ...
>   | declModifiers
>     abbrev declId optDeclSig where
>       structInstField*
> ```
> 
> 在[模块](https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules/#--tech-term-module)中，使用 `abbrev` 的常量声明的主体
> 默认情况下会被暴露。
> 

{{< labelindex 
  type="术语" 
  id_alias="不透明常量"
  title_alias="不透明常量 Opaque Constant"
/>}}**不透明常量 Opaque Constant** 是那些在内核中不受 
[δ 归约]({{< relref "read-LeanRef-web-Chpt04.md" >}}#术语-项的δ归约)影响的已声明常量。
它们在指定某个函数的存在性时非常有用。
  与公理有所不同的是，不透明声明只能用于居留类型，
    因此它们不会引入不一致性；同样
  与公理有所不同的是，类型的居留项会被用于编译后的代码中。
`implemented_by` 属性可以用来指示编译器
在编译不透明常量时
发起对某个其他函数的调用。

{{< labelindex 
  type="语法" 
  id_alias="不透明常量声明"
>}}
`… opaque … := …`\
`… opaque …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
不透明常量声明会如同其他常量声明一样被阐述。
这表明了类型是居留的。居留项的作用止步于此，不会再起其他作用。

```lean {wrapper=false, lineNos=false}
command ::= ...
  | declModifiers
    opaque declId declSig := term
```

不透明常量声明也可以不提供 `:=` 的右侧内容；
阐述器会通过合成一个 `Inhabited` 的实例来填充右侧内容，
如果失败，那么就会尝试合成一个 `Nonempty` 的实例。

```lean {wrapper=false, lineNos=false}
command ::= ...
  | declModifiers
    opaque declId declSig
```
{{< /admonition >}}

## 7.4. 定理声明 Theorems {#S7-4}
{{< ctx level="2" >}}

由于[命题]({{< relref "read-LeanRef-web-Chpt04.md" >}}#术语-命题类型)是类型，
其下的居留项可被视为证明，
因此从技术层面讲定理和定义非常相似。然而，
由于它们的使用场景有很大不同，在许多细节上它们也有所区别：

- 定理的陈述必须是一个命题，而
  常量的类型可以位于任意宇宙中。

- 定理的头部（也就是定理的陈述）会在声明主体被阐述之前被完整地阐述。
  区段变量只有在头部中被提及时（或者它们的依赖项被提及时）才会成为定理的形参。
  这可以预防更改证明时不小心改动定理陈述的情形。

- 定理是默认[不可归约的](https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/#--tech-term-Irreducible)。
  因为同一命题的所有证明都是[定义等价的]({{< relref "read-LeanRef-web-Chpt04.md" >}}#术语-项的定义等价性)，
  基本没必要去展开一个定理。

定理可能是递归的，前提是它们满足与[递归函数声明](https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/#recursive-definitions)相同的条件。不过
更常见的做法是使用如 `induction` 或 `fun_induction` 这样的策略。

{{< labelindex 
  type="语法" 
  id_alias="定理声明"
>}}
`… theorem … := …`\
`… theorem … (| … => …)*`\
`… theorem … where …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
定理声明的语法与常量声明的语法类似，
只不过定理声明的头部必须包含一个返回结果类型注解，
而常量声明的头部则可以省略返回结果类型注解。

```lean {wrapper=false, lineNos=false}
command ::= ...
  | declModifiers
    theorem declId declSig := term

command ::= ...
  | declModifiers
    theorem declId declSig
      (| term => term)*

command ::= ...
  | declModifiers
    theorem declId declSig where
      structInstField*
```

在[模块](https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules/#--tech-term-module)中，使用 `theorem` 的定理声明的主体默认情况下不会被暴露。
{{< /admonition >}}

## 7.5. 例子声明 Example Declarations {#S7-5}
{{< ctx level="2" >}}

例子也是一种常量声明，只不过
其是匿名的，并且
会被阐述然后被丢弃。例子
在开发过程中用于增量测试，并且
可以让文件更容易理解。

{{< labelindex 
  type="语法" 
  id_alias="例子声明"
>}}
`… example … := …`\
`… example … (| … => …)*`\
`… example … where …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
```lean {wrapper=false, lineNos=false}
command ::= ...
  | declModifiers
    example optDeclSig := term

command ::= ...
  | declModifiers
    example optDeclSig
      (| term => term)*

command ::= ...
  | declModifiers
    example optDeclSig where
      structInstField*
```
{{< /admonition >}}

## 7.6. Recursive Definitions {#S7-6}
{{< ctx level="2" >}}

## 索引 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/b210b97/