# 翻译-Lean Language Reference-10-类

{{< ctxset prefix="10" >}}
{{< 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="属性" >}}
{{< labelindexset cnt_sect_digits="2" cnt_appr_digit="2" type="例子" cnt_sect_lv_max="2">}}

一个操作具有{{< labelindex 
  type="术语" 
  id_alias="多态性"
  title_alias="多态性 Polymorphic"
>}}
{{< /labelindex >}}**多态性 Polymorphic**
意味着其可被用于多种类型。Lean 当中存在三种多态性：

1.  [宇宙多态性]({{< relref "read-LeanRef-web-Chpt04.md" >}}#术语-宇宙多态性)，
    即声明中的宇宙可以通过多种方式实例化；

2.  参数多态性，
    即函数可以以类型作为（隐式）实参，
    以便允许单段代码可被用于任何类型；

3.  {{< labelindex 
  type="术语" 
  id_alias="特设多态性"
  title_alias="特设多态性 Ad-hoc Polymorphism"
>}}
{{< /labelindex >}}**特设多态性 Ad-hoc Polymorphism**，
    由类实现，当中被重载的操作对于不同类型可能会有不同的实现。

由于 Lean 不允许对类型分情况分析，
因此不论类型实参如何，多态函数都只会实现一致的操作 —— 比如
`List.map` 就不会因为列表中元素为 `String` 或 `Nat`
而突然采取不同的计算方式。当操作无法只通过“统一”方式实现时，
特设多态操作便派上了用场；一个典型用例便是对算术运算符进行重载，
以使其可用于 `Nat`、`Int`、`Float` 及任何其他具有合理加法概念的类型。
特设多态性也可能会牵扯到多种类型；如在给定集合的指定索引处查找值这个操作
就涉及到了集合的类型、索引的类型以及待提取的集合元素的类型。
一个{{< labelindex 
  type="术语" 
  id_alias="类"
  title_alias="类 Type Class"
>}}
{{< /labelindex >}}**类 Type Class** 描述了
  一系列待重载的操作（称为{{< labelindex 
  type="术语" 
  id_alias="类实例方法"
  title_alias="类实例方法 Method"
>}}
{{< /labelindex >}}**方法 Method**）以及
  各种涉及到的类型。

> 类的首次描述出现在 1989 年 Philip Wadler 和 Stephen Blott 发表的论文
> “How to make ad-hoc polymorphism less ad hoc”，收录于第 16 届 POPL 会议论文集中。

类是非常灵活的，操作的重载可能会牵扯到多种类型；比如
对数据结构进行索引这样的操作的重载就可能会针对特定的
  数据结构、索引类型、元素类型，甚至是针对一个
  判断键是否存在于结构中的谓词。 
得益于 Lean 类型系统强大的表达能力，操作的重载
并非仅局限于类型；类甚至还可以通过
普通值、类型族，甚至由谓词或者是命题来参数化。
这些情况在实践中都存在应用场景：

- **自然数字面量 Natural Number Literals**

  `OfNat` 类用于解释自然数面字面量。类实例不仅
    可能会依赖于被实例化的类型，还
    可能会依赖于数字字面量本身。

- **计算效应 Computational Effects**

  像 `Monad` 这样接收函数作为实参的类
  可以用来提供[带有副作用的程序的特殊语法](https://lean-lang.org/doc/reference/latest/Functors___-Monads-and--do--Notation/#monads-and-do)。
  被重载的操作的“类型”实际上是一个类型函数，比如 `Option`、`IO` 或 `Except`。

- **谓词和命题 Predicates and Propositions**

  `Decidable` 类允许 Lean 自动找到一个命题的判定过程。
  这被用作是 `if` 表达式的基础，使其可根据任何可判定的命题进行分支。

尽管普通多态声明的实例化往往只需提供合适的实参即可，
但是使用了类重载的运算符的实例化用的却是{{< labelindex 
  type="术语" 
  id_alias="类实例"
  title_alias="类实例 Instance"
>}}
{{< /labelindex >}}**类实例 Instance**，
后者为某组特定的形参定义了具体的重载操作。
这些{{< labelindex 
  type="术语" 
  id_alias="实例隐式形参"
  title_alias="实例隐式形参 Instance Implicit Parameter"
>}}
{{< /labelindex >}}**实例隐式形参 Instance Implicit Parameter**用方括号表示。在调用处，Lean 要么
  会从可用的候选者中{{< labelindex 
  type="术语" 
  id_alias="类实例合成"
  title_alias="类实例合成 Synthesize"
>}}
{{< /labelindex >}}**合成 Synthesize**
出一个合适的类实例，要么便报错。
由于类实例本身也可能具有类实例形参，因此这个搜索过程可能会是递归的，
并最终产生一个复合的类实例值，该值结合了来自各种类实例的代码。因此，
类实例合成也是一种以类型驱动 Type-Directed 方式构造程序的手段。

下面是一些类的典型用例：

- 类可以用于表示待重载的操作符，比如
    可用于多种类型的数字的算术运算，或者是
    可用于多种数据结构的成员判断谓词。
  通常来说对于给定类型往往只存在一个典范的操作符 ——
  毕竟对 `Nat` 来说加法的定义没有其他合理的替代方案；
  但是这并非一个必要属性，如有必要库也可以提供替代类实例。

- 类可以用于表示一个代数结构及其所需的额外结构以及公理。
  比如一个表示阿贝尔群的类就可能包含
    一个二元运算符、
    一个一元逆运算符、
    一个幺元，外加上
    二元运算符满足结合律和交换律的证明、
    幺元之所以能构成幺元的证明、
    一元逆运算符在运算符两侧都能产生幺元的证明。
  在这里可能不存在一个典范的结构选择，
  库可能会提供多种方式来实例化给定的一组公理；
  比如整数上就存在着两种同样典范的幺半群结构。

- 类可以用于表示两个类型之间的关系，
  使得它们可以一起以某种新颖的方式为库所使用。
  类 `Coe` 被用于表示自动插入的类型强制转换，而
  类 `MonadLift` 被用于表示将具有某种效应的操作运行在期待另一种效应的语境中的方法。

- 类可以用于表示类型驱动的代码生成框架，当中
  各个多态类型的实例都会贡献一部分最终程序的内容。比如
  类 `Repr` 会为每个类型定义一个规范化的美化打印器，而
  多态类型则会拥有多态的 `Repr` 实例。最终
  当美化打印在一个已知具体类型的表达式上被调用时 ——
  比如 `List (Nat × (String ⊕ Int))`，
  生成的美化打印器将会包含从
  `List`、`Prod`、`Nat`、`Sum`、`String`、`Int`
  的 `Repr` 实例中组装而成的代码。

## 10.1. 类声明 Class Declarations {#S10-1}
{{< ctx level="2" >}}

类的声明通过 `class` 关键字来实现。

{{< labelindex 
  type="语法" 
  id_alias="类声明"
>}}
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
```lean {wrapper=false, lineNos=false}
command ::= ...
  | declModifiers
    class declId bracketedBinder* (: term)?
      (extends (ident : )?term,*)?
      where
      (declModifiers ident ::)?
      structFields
    (deriving ident,*)?
```

会声明一个新的类。
{{< /admonition >}}

`class` 命令会创建一个新的只有单个归纳项构造子的归纳类型构造子，就如同使用
`structure` 命令一样。事实上 `class` 和 `structure` 的效果几乎是相同的，并且
在两者中可以以相同的方式使用默认值等功能。有关结构继承、字段的默认值等其他功能的更多信息
请见[此处]({{< relref "read-LeanRef-web-Chpt04.md" >}}#S4-4-2)。
结构声明与类声明之间的区别如下：

- **方法而非字段被创建**

  类声明不会创建以类实例为实参的投影函数；相反，
  类声明会创建[类实例方法](#术语-类实例方法)，
  每个类实例方法都会将对应的实例用作是实例隐式形参。

- **父类是实例隐式的**

  对于那些继承自其他类的类，它们的类实例构造子
  会将其父类实例用作是实例隐式形参而非显式形参：
  当该类的实例被声明时，类实例合成会被用来寻找那些被继承过来的字段的值。
  至于那些不是类的父结构则仍然是底层构造子的显式形参。

- **父投影函数是由类实例合成生成的**

  结构项投影会利用[继承信息]({{< relref "read-LeanRef-web-Chpt04.md" >}}#S4-4-2-4)
  从子结构项中投影出父结构项。
  类用的则是类实例合成：给定一个子类实例，类实例合成会构造父类；
  因此，类实例方法不会像项投影函数被添加到子结构那样被添加到子类当中。

- **归纳会被注册为类**

  归纳声明后的结果会被注册为一个类，如此便可
  为其声明类实例并将该实例用作实例隐式形参。

- **输出参数和半输出参数会被考虑**

  尽管零件 `outParam` 和 `semiOutParam` 
  在结构声明中没有意义，但是
  在类声明中它们被用来控制类实例搜索。

虽然 `deriving` 子句被允许用于类定义
以保持类声明和结构声明之间的平行性，
但是实际上它们并不常用，
并且应被视为一个高级特性。

{{< labelindex 
  type="例子" 
  summary="只有类才能有实例"
>}}
示范：`def f [n : Nat] : n = n := rfl`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：只有类才能有实例"
  open=false
>}}
Lean 会拒绝那些类型非类类型的实例隐式形参：

```lean {wrapper=false, lineNos=false}
def f [n : Nat] : n = n := rfl

-- invalid binder annotation, type is not a class instance
--  Nat
-- Note: Use the command `set_option checkBinderAnnotations false` to 
-- disable the check
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="类实例构造子和结构项构造子的区别"
>}}
示范：`S`、`C1.Monoid`、`C2.Magma`、`C2.Semigroup`、`C2.Monoid`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类实例构造子和结构项构造子的区别" 
  open=false
>}}
一个非常小的代数层次结构
既可以全部用结构表示（如下面的 `S.Magma`、`S.Semigroup`、`S.Monoid`）
也可以用结构和类混合表示（如下面的 `C1.Monoid`）
还可以全部都用类表示（如下面的 `C2.Magma`、`C2.Semigroup`、`C2.Monoid`）：

```lean {wrapper=false, lineNos=false}
namespace S
structure Magma (α : Type u) where
  op : α → α → α

structure Semigroup (α : Type u) extends Magma α where
  op_assoc : ∀ x y z, op (op x y) z = op x (op y z)

structure Monoid (α : Type u) extends Semigroup α where
  ident : α
  ident_left : ∀ x, op ident x = x
  ident_right : ∀ x, op x ident = x
end S

namespace C1
class Monoid (α : Type u) extends S.Semigroup α where
  ident : α
  ident_left : ∀ x, op ident x = x
  ident_right : ∀ x, op x ident = x
end C1

namespace C2
class Magma (α : Type u) where
  op : α → α → α

class Semigroup (α : Type u) extends Magma α where
  op_assoc : ∀ x y z, op (op x y) z = op x (op y z)

class Monoid (α : Type u) extends Semigroup α where
  ident : α
  ident_left : ∀ x, op ident x = x
  ident_right : ∀ x, op x ident = x
end C2
```

`S.Monoid` 的结构项构造子和 
`C1.Monoid` 的类实例构造子具有相同的签名，这是因为
`C1.Monoid` 的父结构 `S.Semigroup` 本身并不是类：

```lean {wrapper=false, lineNos=false}
#check S.Monoid.mk -- 继承自 S.Semigroup
-- S.Monoid.mk.{u} {α : Type u}
-- (toSemigroup : S.Semigroup α) (ident : α)
-- (ident_left  : ∀ (x : α), toSemigroup.op ident x = x)
-- (ident_right : ∀ (x : α), toSemigroup.op x ident = x)
-- : S.Monoid α

#check C1.Monoid.mk -- 继承自 S.Semigroup
-- C1.Monoid.mk.{u} {α : Type u}
-- (toSemigroup : S.Semigroup α)
-- (ident : α)
-- (ident_left  : ∀ (x : α), toSemigroup.op ident x = x)
-- (ident_right : ∀ (x : α), toSemigroup.op x ident = x)
-- : C1.Monoid α
```

出于类似的原因，
`S.Magma` 的结构项构造子和
`C2.Magma` 的类实例构造子是相同的；
因为它们都没有继承自其他结构或类。

```lean {wrapper=false, lineNos=false}
#check S.Magma.mk
-- S.Magma.mk.{u} {α : Type u}
-- (op : α → α → α)
-- : S.Magma α

#check C2.Magma.mk
-- C2.Magma.mk.{u} {α : Type u}
-- (op : α → α → α)
-- : C2.Magma α
```

然而 
`S.Semigroup` 会取其父结构下的项作为显式形参，而
`C2.Semigroup` 却会取其父类下的实例作为实例隐式形参。

```lean {wrapper=false, lineNos=false}
#check S.Semigroup.mk -- 继承自 S.Magma
-- S.Semigroup.mk.{u} {α : Type u}
-- (toMagma : S.Magma α)
-- (op_assoc : ∀ (x y z : α), toMagma.op (toMagma.op x y) z = toMagma.op x (toMagma.op y z))
-- : S.Semigroup α

#check C2.Semigroup.mk -- 继承自 C2.Magma
-- C2.Semigroup.mk.{u} {α : Type u}
-- [toMagma : C2.Magma α]
-- (op_assoc : ∀ (x y z : α), C2.Magma.op (C2.Magma.op x y) z = C2.Magma.op x (C2.Magma.op y z))
--   C2.Magma.op x y 会变成 @C2.Magma.op α toMagma x y
-- : C2.Semigroup α
```

最终 `C2.Monoid.mk` 会取其父类（半群）下的实例作为实例隐式参数。
另外对 `op` 的引用会转变为对方法 `C2.Magma.op` 的引用，这一切
需要依赖类实例合成借助实例隐式形参 `toSemigroup` 的父投影来恢复实现。

```lean {wrapper=false, lineNos=false}
#check C2.Monoid.mk -- 继承自 C2.Semigroup
-- C2.Monoid.mk.{u} {α : Type u}
-- [toSemigroup : C2.Semigroup α]
-- (ident : α)
-- (ident_left : ∀ (x : α), C2.Magma.op ident x = x)
-- (ident_right : ∀ (x : α), C2.Magma.op x ident = x)
--   C2.Magma.op x y 会变成 @C2.Magma.op α toSemigroup.toMagma x y
-- : C2.Monoid α
```
{{< /admonition >}}

类类型构造子的形参可通过{{< labelindex 
  type="术语" 
  id_alias="零件"
  title_alias="零件 Gadget"
>}}
{{< /labelindex >}}**零件 Gadget** 来标记。
零件是特殊的恒等函数，它会使阐述器以不同的方式来处理一个值。
零件并不会改变一个项的**含义**，但是
它们可能导致在阐述时的搜索程序中项会以不同的方式被处理。
零件 `outParam` 和 `semiOutParam` 会影响[类实例合成](#S10-3)，
它们在类实例合成有关的那一章节中会被详细介绍。

一个类型不论是否构成类类型都不会影响定义等价性。
即便一个类的类型构造子的实参是一样的，
该类的两个实例也未必是相同的，甚至还可能会有很大的不同。

{{< labelindex 
  type="例子" 
  summary="类类型下的实例不唯一所导致的问题"
>}}
示范：`Ord`，`Heap`，`Heap'`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类类型下的实例不唯一所导致的问题" 
  open=false
>}}
下述二叉堆插入的实现充满了不少问题：

```lean {wrapper=false, lineNos=false}
structure Heap (α : Type u) where
  contents : Array α
deriving Repr

def Heap.bubbleUp [Ord α] (i : Nat) (xs : Heap α) : Heap α :=
  if h : i = 0 then xs
  else if h : i ≥ xs.contents.size then xs
  else
    let j := i / 2
    if Ord.compare xs.contents[i] xs.contents[j] == .lt then
      Heap.bubbleUp j { xs with contents := xs.contents.swap i j }
    else xs

def Heap.insert [Ord α] (x : α) (xs : Heap α) : Heap α :=
  let i := xs.contents.size
  {xs with contents := xs.contents.push x}.bubbleUp i
```

问题在于：使用一个 `Ord` 类实例构造的堆
可能会在之后被用于另一个类实例，从而破坏堆的不变性。
一个解决办法是让堆类型依赖于所选的 `Ord` 类实例：

```lean {wrapper=false, lineNos=false}
structure Heap' (α : Type u) [Ord α] where
  contents : Array α

def Heap'.bubbleUp [inst : Ord α]
    (i : Nat) (xs : @Heap' α inst) :
    @Heap' α inst :=
  if h : i = 0 then xs
  else if h : i ≥ xs.contents.size then xs
  else
    let j := i / 2
    if inst.compare xs.contents[i] xs.contents[j] == .lt then
      Heap'.bubbleUp j {xs with contents := xs.contents.swap i j}
    else xs

def Heap'.insert [Ord α] (x : α) (xs : Heap' α) : Heap' α :=
  let i := xs.contents.size
  {xs with contents := xs.contents.push x}.bubbleUp i
```

改进后代码中的 `Heap'.bubbleUp` 显得过于明确（显式）；
隐式实例形参在这里没必要被显式地声明为 `inst`，
因为 Lean 仍然会选中被指定的类实例。
但这么做确实向读者强调了正确的不变量。
{{< /admonition >}}

### 10.1.1. 和类型作为类 Sum Types as Classes {#S10-1-1}
{{< ctx level="3" >}}

大多数类都遵循一种范式：它们都描述了一组可被重载的类实例方法，
用户可以自由地在这些实例方法中进行选择；
自然地这会被建模为一个积类型，当中的类实例方法便是投影。尽管如此，
有一些类却是和类型：它们要求被合成的实例的接收者
首先检查**哪一个**可用的类实例构造子会被提供。为了将这些类考虑进去，
类声明也可以包含任意的[归纳类型]({{< relref "read-LeanRef-web-Chpt04.md" >}}#术语-归纳类型)，而不仅仅是作为结构声明的扩展形式而已。

{{< labelindex 
  type="语法" 
  id_alias="归纳类声明"
>}}
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
```lean {wrapper=false, lineNos=false}
command ::= ...
  | declModifiers
    class inductive declId optDeclSig where
      (| declModifiers ident optDeclSig)*
    (deriving ident,*)?
```
{{< /admonition >}}

归纳类类型就像其他归纳类型一样，只不过它们可能会参与类实例的合成。
一个归纳类的典型例子是 `Decidable`：在含有自由变量的语境当中，
合成一个类实例就相当于是合成对应的判定过程；但是如果没有自由变量，
那么命题的真值就可以仅通过类实例合成来确定（正如 `decide` 策略所做的那样）。

### 10.1.2. 类的缩写 Class Abbreviations  {#S10-1-2}
{{< ctx level="3" >}}

某些情况下，代码库中可能到处都存在着彼此相关联的类。与其重复地写下所有的名称，
不如直接声明一个继承了所有彼此相关联的类且不贡献任何新实例方法的类？然而这个
新声明的类有个缺点：它的实例必须被显式声明。

命令 `class abbrev` 允许声明类缩写，当中
被创建的名称就是其他一系列类的简写。类缩写在背后
是由一个继承了其他类的类所表示的，此外与其对应的
实例构造子还被额外声明为实例，如此新的类也就可以
只通过实例合成来构造了。

{{< labelindex 
  type="例子" 
  summary="类缩写声明与类声明的区别"
>}}
示范：`Add`，`Mul`，`AddMul`，`AddMul'`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类缩写声明与类声明的区别" 
  open=false
>}}
`plusTimes1` 和 `plusTimes2` 各自都带有一个隐式实例形参，
分别是 `AddMul α` 和 `AddMul' α`：

```lean {wrapper=false, lineNos=false}
class abbrev AddMul (α : Type u) := Add α, Mul α
def plusTimes1 [AddMul α] (x y z : α) := x + y * z

class AddMul' (α : Type u) extends Add α, Mul α
def plusTimes2 [AddMul' α] (x y z : α) := x + y * z
```

由于 `AddMul` 是一个类缩写，
因此无需额外的类实例声明即可将 `plusTimes1` 应用到自然数项上：

```lean {wrapper=false, lineNos=false}
#eval plusTimes1 2 5 7
-- 37
```

但是 `plusTimes2` 却导致报错，因为
不存在 `AddMul' Nat` 实例——至少目前为止还未声明任何类实例：

```lean {wrapper=false, lineNos=false}
#eval plusTimes2 2 5 7
-- failed to synthesize instance of type class
--  AddMul' ?m.8
-- 
-- Hint: Type class instance resolution failures 
-- can be inspected with the 
-- `set_option trace.Meta.synthInstance true` command.
```

声明一个非常通用的类实例即可解决 `Nat` 以及其他所有类型的问题：

```lean {wrapper=false, lineNos=false}
instance [Add α] [Mul α] : AddMul' α where

#eval plusTimes2 2 5 7
-- 37
```
{{< /admonition >}}

## 10.2. 类实例声明 Instance Declarations {#S10-2}
{{< ctx level="2" >}}

类实例声明的语法和常量声明的语法几乎是一样的，唯一的区别仅在于
  关键字 `def` 被替换为 `instance`，并且
  类实例的名称是可选的：

{{< labelindex 
  type="语法" 
  id_alias="类实例声明"
>}}
`instance ((priority := …))? … where …`\
`instance ((priority := …))? … := …`\
`instance ((priority := …))? … (| … => …)*`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
大部分类实例都是通过 `where` 来定义各个类实例方法的：

```lean {wrapper=false, lineNos=false}
instance ::= ...
  | instance ((priority := prio))? declId? declSig where
      structInstField*
```

尽管如此，由于类本身是归纳，
因此类实例也可以通过任何具有适当类型的项来构造：

```lean {wrapper=false, lineNos=false}
instance ::= ...
  | instance ((priority := prio))? declId? declSig :=
      term
```

类实例也可以通过分类讨论来声明；然而
除了 `Decidable` 实例外这个特性很少被使用：

```lean {wrapper=false, lineNos=false}
instance ::= ...
  | instance ((priority := prio))? declId? declSig
      (| term => term)*
```
{{< /admonition >}}

通常来说，带有显式项的类实例声明包含的内容要么是
  对结构项构造子的匿名调用（`⟨...⟩`），不然就是
  在彼此定义等价的类型上调用 `inferInstanceAs`。

类实例的阐述几乎与普通常量的阐述一致，只不过
还需要注意下面所列的注意事项。
如果没有提供类实例名称，那么一个名称会被自动创建：
这个生成的名称可被引用，但是生成名称所使用的算法
在过去曾发生过变化，并且在未来也可能会发生变化；
因此最好是显式地命名那些将会被直接引用的类实例。
新的类实例在被阐述之后会被注册为类实例搜索的候选者。
为一个名称补充属性 `instance` 可以用来
将任何其他已声明的名称标记为候选者。

{{< labelindex 
  type="例子" 
  summary="类实例名称的自动生成"
>}}
示范：`BEq`，`NatWrapper`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类实例名称的自动生成" 
  open=false
>}}
对于下述声明：

```lean {wrapper=false, lineNos=false}
structure NatWrapper where
  val : Nat

instance : BEq NatWrapper where -- 鼠标悬浮在 instance 上即可看到 instBEqNatWrapper
  beq
    | ⟨x⟩, ⟨y⟩ => x == y
```

名称 `instBEqNatWrapper` 即为自动生成的新的类实例。
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="类实例声明的各种变体"
>}}
示范：`BEq`，`NatWrapper`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类实例声明的各种变体" 
  open=false
>}}
给定下述结构：

```lean {wrapper=false, lineNos=false}
structure NatWrapper where
  val : Nat
```

下述各种 `BEq` 类实例的声明都是彼此等价的：

```lean {wrapper=false, lineNos=false}
instance : BEq NatWrapper where
  beq
    | ⟨x⟩, ⟨y⟩ => x == y

instance : BEq NatWrapper :=
  ⟨fun x y => x.val == y.val⟩

instance : BEq NatWrapper :=
  ⟨fun ⟨x⟩ ⟨y⟩ => x == y⟩
```

除了向环境引入不同的名称之外，
下述声明也是彼此等价的：

```lean {wrapper=false, lineNos=false}
@[instance]
def instBeqNatWrapper : BEq NatWrapper where
  beq
    | ⟨x⟩, ⟨y⟩ => x == y

instance : BEq NatWrapper :=
  ⟨fun x y => x.val == y.val⟩

instance : BEq NatWrapper :=
  ⟨fun ⟨x⟩ ⟨y⟩ => x == y⟩
```
{{< /admonition >}}

### 10.2.1. 递归类实例 Recursive Instances {#S10-2-1}
{{< ctx level="3" >}}

在 `where` 结构项声明语法中定义的函数不可以是递归的。
而由于类实例声明是结构项声明的其中一种形式，
因此类实例方法默认也不可以是递归的。尽管如此，
递归归纳类的实例却非常常见。有一个标准的惯用法可以绕过这个限制：
可以先在类实例声明外声明一个递归函数，
然后再在类实例声明中引用它。按照惯例，
这些递归函数与对应的类实例方法应具有相同的名称，
只不过前者的声明发生在类对应的命名空间中。

{{< labelindex 
  type="例子" 
  summary="类实例声明为递归的"
>}}
示范：`BEq`，`NatTree`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类实例声明为递归的" 
  open=false
>}}
提供一个归纳声明 `NatTree`：

```lean {wrapper=false, lineNos=false}
inductive NatTree where
  | leaf
  | branch (left : NatTree) (val : Nat) (right : NatTree)
```

下述 `BEq` 的类实例会导致报错，
左（`l1 == l2`）右（`r1 == r2`）两处的递归调用都会导致报错：

```lean {wrapper=false, lineNos=false}
instance : BEq NatTree where
  beq
    | .leaf, .leaf =>
      true
    | .branch l1 v1 r1, .branch l2 v2 r2 =>
      l1 == l2 && v1 == v2 && r1 == r2 -- 这里报错了
    | _, _ =>
      false
-- failed to synthesize instance of type class
--  BEq NatTree
-- 
-- Hint: Adding the command `deriving instance BEq for 
-- NatTree` may allow Lean to derive the missing instance.
```

给定一个合适的递归函数 `NatTree.beq`：

```lean {wrapper=false, lineNos=false}
def NatTree.beq : NatTree → NatTree → Bool
  | .leaf, .leaf =>
    true
  | .branch l1 v1 r1, .branch l2 v2 r2 =>
    NatTree.beq l1 l2 && v1 == v2 && NatTree.beq r1 r2
  | _, _ =>
    false
```

接下来我们就可以声明类实例了：

```lean {wrapper=false, lineNos=false}
instance : BEq NatTree where
  beq := NatTree.beq
```

使用归纳项构造子的匿名调用语法也可以实现同样的效果：

```lean {wrapper=false, lineNos=false}
instance : BEq NatTree := ⟨NatTree.beq⟩
```
{{< /admonition >}}

不仅如此，类实例在其自身的声明中也不可以被用于类实例合成。
只有在被声明之后它们才会被标记为可用于实例合成。在嵌套的归纳类型当中，
如果递归出现的类型正好是某个其他归纳类型构造子的实参，
那么要编写递归函数可能还需要先声明一个类实例。
一个惯用的解决方法是在递归函数的声明主体内先局部声明一个类实例，
这个局部类实例包含了对正在被声明的函数的引用，
如此一来类实例合成便可以正确的类型使用局部语境中的每个绑定。

{{< labelindex 
  type="例子" 
  summary="类实例与嵌套归纳类型有关的情况"
>}}
示范：`BEq`，`NatRoseTree`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类实例与嵌套归纳类型有关的情况" 
  open=false
>}}
在下述 `NatRoseTree` 的声明中，待声明的类型的名称
嵌套出现在另一个归纳类型构造子 `Array` 的实参中：

```lean {wrapper=false, lineNos=false}
inductive NatRoseTree where
  | node (val : Nat) (children : Array NatRoseTree)
```

检查 `NatRoseTree` 下的项的等价性需要检查 `Array` 的等价性。
但是由于类实例在它们自己的声明中通常是无法被用于实例合成的，
因此下面的常量声明会导致报错 —— 即便 `NatRoseTree.beq` 
  是一个递归函数并且其
  位于自身声明中的作用域内。

```lean {wrapper=false, lineNos=false}
def NatRoseTree.beq : (tree1 tree2 : NatRoseTree) → Bool
  | .node val1 children1, .node val2 children2 =>
    val1 == val2 &&
    children1 == children2 -- 这里有个实例声明？ Beq NatRoseTree
-- failed to synthesize instance of type class
--   BEq (Array NatRoseTree)
-- 
-- Hint: Type class instance resolution failures 
-- can be inspected with the 
-- `set_option trace.Meta.synthInstance true` command.
```

要解决这个问题，我们可以通过 `let` 来
绑定一个局部的 `BEq NatRoseTree` 实例：

```lean {wrapper=false, lineNos=false}
partial def NatRoseTree.beq : (tree1 tree2 : NatRoseTree) → Bool
  | .node val1 children1, .node val2 children2 =>
    let _ : BEq NatRoseTree := ⟨NatRoseTree.beq⟩
    val1 == val2 &&
    children1 == children2
```

如此 `children1 == children2` 的检查
就可以在实例合成期间找到由 `let` 绑定的实例。
{{< /admonition >}}

### 10.2.2. 归纳类实例 Instances of `class inductives` {#S10-2-2}
{{< ctx level="3" >}}

许多类实例具有函数类型：
任何会递归调用类实例搜索的类实例本身就构成一个函数，
具有隐式形参的类实例也是如此。
虽然大多数类实例只会从它们自己的实例形参中投射出类实例方法的实现，
但是归纳类类型的类实例通常会对它们的一个或多个实参进行模式匹配，
从而允许类实例选择适当的类实例构造子。
这是通过普通的 Lean 函数语法来实现的。与其他类实例一样，
正在被讨论的函数在它自身的声明中并不可以被用于类实例合成。

{{< labelindex 
  type="例子" 
  summary="归纳类的实例"
>}}
示范：`DecidableEq`，`ThreeChoices`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：归纳类的实例" 
  open=false
>}}
由于 `DecidableEq α` 是 `(a b : α) → Decidable (Eq a b)` 的缩写，
因此它的实参可以被直接使用，如下所示：

```lean {wrapper=false, lineNos=false}
inductive ThreeChoices where
  | yes | no | maybe

instance : DecidableEq ThreeChoices
  | .yes,   .yes   =>
    .isTrue rfl
  | .no,    .no    =>
    .isTrue rfl
  | .maybe, .maybe =>
    .isTrue rfl
  | .yes,   .maybe | .yes,   .no
  | .maybe, .yes   | .maybe, .no
  | .no,    .yes   | .no,    .maybe =>
    .isFalse nofun
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="归纳类实例声明为递归的"
>}}
示范：`DecidableEq`，`StringList`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：归纳类实例声明为递归的" 
  open=false
>}}
归纳 `StringList` 用于表示字符串的单态列表：

```lean {wrapper=false, lineNos=false}
inductive StringList where
  | nil
  | cons (hd : String) (tl : StringList)
```

在下述声明 `DecidableEq` 类实例的尝试中，
在阐述第二层的 `if` 时类实例合成会失败；
这是因为类实例在其自身的声明中并不可用于类实例合成：

```lean {wrapper=false, lineNos=false}
instance : DecidableEq StringList
  | .nil, .nil => .isTrue rfl
  | .cons h1 t1, .cons h2 t2 =>
    if h : h1 = h2 then
      if h' : t1 = t2 then
        .isTrue (by simp [*])
      else
        .isFalse (by intro hEq; cases hEq; trivial)
    else
      .isFalse (by intro hEq; cases hEq; trivial)
  | .nil, .cons _ _ | .cons _ _, .nil => .isFalse nofun
-- failed to synthesize instance of type class
--   Decidable (t1 = t2)
-- 
-- Hint: Type class instance resolution failures can be inspected 
-- with the `set_option trace.Meta.synthInstance true` command.
```

然而由于它只是一个普通的 Lean 函数，
因此它可以递归地引用自身显式提供的名称：

```lean {wrapper=false, lineNos=false}
instance instDecidableEqStringList : DecidableEq StringList
  | .nil, .nil => .isTrue rfl
  | .cons h1 t1, .cons h2 t2 =>
    let _ : Decidable (t1 = t2) :=
      instDecidableEqStringList t1 t2
    if h : h1 = h2 then
      if h' : t1 = t2 then
        .isTrue (by simp [*])
      else
        .isFalse (by intro hEq; cases hEq; trivial)
    else
      .isFalse (by intro hEq; cases hEq; trivial)
  | .nil, .cons _ _ | .cons _ _, .nil => .isFalse nofun
```
{{< /admonition >}}

### 10.2.3. 类实例优先级 Instance Priorities {#S10-2-3}
{{< ctx level="3" >}}

类实例可以被赋予{{< labelindex 
  type="术语" 
  id_alias="类实例优先级"
  title_alias="类实例优先级 Priority"
>}}
{{< /labelindex >}}**优先级 Priority**。在类实例合成期间，
那些具有更高优先级的实例会被优先考虑。
有关类实例合成的详细信息请参阅[类实例合成](#S10-3)一节。

{{< labelindex 
  type="语法" 
  id_alias="类实例声明（优先级补充）"
>}}
`default`\
`low`\
`mid`\
`high`\
`(…)`\
`… + …`\
`… - …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
类实例优先级可以是数字：

```lean {wrapper=false, lineNos=false}
prio ::=
    num
```

如果没有指定优先级，那么优先级的默认值（`1000`）将被使用：

```lean {wrapper=false, lineNos=false}
prio ::= ...
  | default
```

在默认值数值粒度太细的时候有三种命名优先级可供选择，
分别对应于 `100`、`500` 和 `10000`。
其中 `mid` 优先级低于 `default`。

```lean {wrapper=false, lineNos=false}
prio ::= ...
  | low

prio ::= ...
  | mid

prio ::= ...
  | high
```

此外优先级还可以进行加减法运算，
因此 `default + 2` 是一个有效的优先级，对应于 `1002`。

```lean {wrapper=false, lineNos=false}
prio ::= ...
  | (prio)

prio ::= ...
  | prio + prio

prio ::= ...
  | prio - prio
```
{{< /admonition >}}

### 10.2.4. 类默认实例 Default Instances {#S10-2-4}
{{< ctx level="3" >}}

属性 `default_instance` 用于指定
[在缺乏足够信息来选择类实例的情况下应使用哪个类实例作为默认回退值](#S10-3-6)。
如果没有指定优先级，那么类实例优先级的默认值 `default` 将会被使用。

{{< labelindex 
  type="属性" 
  id_alias="default_instance"
>}}
设置类默认实例及其对应的优先级
{{< /labelindex >}}
{{< admonition 
  type=info
  title="属性：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
attr ::= ...
  | default_instance prio?
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="类默认实例优先级的设置"
>}}
示范：`OfNat`，`Even`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类默认实例优先级的设置" 
  open=false
>}}
`OfNat Nat` 类的默认实例能够让自然数字面量
在缺乏其他类型信息的情况下被解释为 `Nat` 类型。
它在 Lean 的标准库中被声明，并且优先级被设置为 `100`。
考虑下述偶数的表示形式，其中偶数由其自身的一半所表示：

```lean {wrapper=false, lineNos=false}
structure Even where
  half : Nat
```

下述类实例声明允许数字字面量被用于较小的 `Even` 值
（类实例搜索的深度限制阻止它们被用于任意大的字面量）：

```lean {wrapper=false, lineNos=false}
instance ofNatEven0 : OfNat Even 0 where
  ofNat := ⟨0⟩

instance ofNatEvenPlusTwo [OfNat Even n] : OfNat Even (n + 2) where
  ofNat := ⟨(OfNat.ofNat n : Even).half + 1⟩

#eval (0 : Even)
-- { half := 0 }
#eval (34 : Even)
-- { half := 17 }
#eval (254 : Even)
-- { half := 127 }
```

将它们的类默认实例优先级设置为大于等于 `100`
会导致在没有类型提示的时候会优先使用 `Even` 而非 `Nat`：

```lean {wrapper=false, lineNos=false}
attribute [default_instance 100] ofNatEven0
attribute [default_instance 100] ofNatEvenPlusTwo
#eval 0
-- { half := 0 }
#eval 34
-- { half := 17 }
```

非偶数数字则仍然会使用 `OfNat Nat` 作为类实例：

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

### 10.2.5. `instance` 属性 The Instance Attributes {#S10-2-5}
{{< ctx level="3" >}}

属性 `instance` 用于将一个声明转变为类实例。和其他属性一样，
它可以被应用于全局、局部，或者是仅在当前命名空间被打开时生效。
`instance` 命令就是一种会自动应用 `instance` 属性的常量声明形式。

{{< labelindex 
  type="属性" 
  id_alias="instance"
>}}
将常量声明为类实例并指定类实例优先级
{{< /labelindex >}}
{{< admonition 
  type=info
  title="属性：`{{< indexprint >}}`" 
>}}
将其所作用于的声明转变为一个类实例。
如果优先级未被提供，那么默认的优先级 `default` 将会被使用。

```lean {wrapper=false, lineNos=false}
attr ::= ...
  | instance prio?  
```
{{< /admonition >}}

## 10.3. 类实例合成 Instance Synthesis {#S10-3}
{{< ctx level="2" >}}

类实例合成是一个递归的搜索过程：其要么
为给定的类构造出一个实例，要么失败。换句话说，
给定一个被注册为类的东西，类实例合成会尝试构造一个居留于该类类型下的项。
类实例合成遵循[可约性](https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/#--tech-term-reducibility)：
[半可约](https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/#--tech-term-Semireducible)或
[不可约](https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/#--tech-term-Irreducible)
的常量声明不会被展开，
因此除非是可约的，否则一个被声明的类实例不会被自动视为其展开结果。此外
同一个类类型可能会有多个可能的实例；这种情况下类实例优先级和类实例声明顺序会被用作裁决依据；
按照这个规则，对于一系列具有相同优先级的类实例来说，最近声明的那个会被优先考虑。

这个搜索过程
  在**菱形 Diamond** 存在的情况下是高效的，并且
  在**回环 Cycle** 存在的情况下也不会陷入无限循环。
  菱形会在存在多条通向给定目标的路径时出现，而
  回环则指的是两个类实例中只要其中一个可以被解决另一个便迎刃而解的情况。
  菱形在实践中会经常出现，比如考虑使用类来描述数学概念的情形；而
  回环常常会由 Lean 的类型强制转换特性自然产生，比如有限集和有限多重集之间的强制类型转换。

`#synth` 命令可以用于测试类实例合成，而
`inferInstance` 和 `inferInstanceAs` 则可用于在需要类实例的位置合成出一个实例。
带有类型注解的 `inferInstance` 与 `inferInstanceAs` 并不等价：
后者会[预处理合成的实例](#S10-3-8)
以防止实现细节意外泄漏到接口当中。

{{< labelindex 
  type="常量" 
  id_alias="inferInstance"
>}}
同 `id` 但是会使用类实例合成
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
inferInstance.{u} {α : Sort u} [i : α] : α
```

`inferInstance` 会通过类实例合成来合成出一个任意目标类型下的值。
这个函数具有与恒等函数相同的类型签名，只不过
`[i : α]` 参数上的方括号意味着
它会尝试通过类实例合成来构造这个实参
（若 `α` 不构成一个类类型则操作失败）。示例：

```lean {wrapper=false, lineNos=false}
#check (inferInstance : Inhabited Nat) 
-- Inhabited Nat
@[instance_reducible]
def foo : Inhabited (Nat × Nat) := inferInstance

example : foo.default = (default, default) := rfl
```
{{< /admonition >}}

{{< labelindex 
  type="常量" 
  id_alias="inferInstanceAs"
>}}
合成一个类实例并将其调整为符合预期类型
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
«inferInstanceAs».{u} (α : Sort u) [i : α] : α
```

`inferInstanceAs α` 会合成出一个类型为 `α` 的类实例，然后
将其调整为符合预期类型 `β`。`β` 必须是可以从语境中推断出来的。

例如：

```lean{wrapper=false, lineNos=false}
def D := Nat

instance : Inhabited D := inferInstanceAs (Inhabited Nat)
```

这种调整会确保最终得到的类实例在透明度低于 `semireducible` 的情况下
不会泄漏右手边的 `Nat`；也就是说 `D` 也不会被展开，从而预防了“定义等价性的滥用”。

更具体地说，给定
  “源头类型”（实参）和
  “目标类型”（预期类型），
`inferInstanceAs` 会为源类型合成出一个实例，然后
根据需要展开并重新包装其组件（结构字段、嵌套类实例等）
以使它们与目标类型兼容。各个步骤由以下各个选项所表示，
每个选项都默认会被启用，并且
每个选项可被禁用以便移植代码：

- `backward.inferInstanceAs.wrap`: \
  总开关，决定是否在
  `inferInstanceAs` 和
  默认类实例派生处理器 `deriving` 内
  启用类实例调整；

- `backward.inferInstanceAs.wrap.reuseSubInstances`: \
  决定在字段为子类实例时是否为其复用子类类型下已有的类实例，
  以避免菱形中出现非定义等价的类实例；

- `backward.inferInstanceAs.wrap.instances`: \
  决定是否将不可约类实例包装在辅助声明当中；

- `backward.inferInstanceAs.wrap.data`: \
  若字段为数据项则将其包装在辅助声明当中，
  若字段为证明则总将其包装在辅助定理当中；

如果你只是想合成一个类实例并且不需要进行类型间的转换，
那么请使用 `inferInstance`，并且请在必要时为预期类型提供类型注解。
{{< /admonition >}}

### 10.3.1. 类实例搜索概要 Instance Search Summary {#S10-3-1}
{{< ctx level="3" >}}

一般来说类实例合成是一个会随意回溯的递归搜索过程。类实例合成可能
  **成功**（如果一个类实例项被找到），也可能
  **失败**（如果这样的项无法被找到），或者是
  **卡住**（如果信息不足）。
有关类实例合成算法的详细描述可参考 Selsam, Ullrich, 和 de Moura (2020) 的[预印本“Tabled Typeclass Resolution”](https://arxiv.org/abs/2001.04301)。
一个类实例搜索问题会在一个类类型构造子应用于具体实参时被引入；
这些实参值可能已知，也可能未知。类实例搜索会
  尝试每个局部绑定的、类型为类类型的变量，也会按照类实例优先级和类实例声明的先后顺序
  尝试每个已注册的类实例。
如果候选的类实例本身还带有实例隐式形参，
那么它们还会引入后续的的类实例合成任务。

一个类实例搜索问题只有在类类型构造子的所有输入实参都已知的情况下才会被尝试。
如果一个问题还无法被尝试，那么该分支就会卡住；
其他子问题的进展可能会使得该问题变得可解。
在类实例搜索开始时，输出或半输出实参可能是已知的，也可能是未知的。
输出实参在 Lean 检查一个类实例是否匹配类实例搜索问题的时候会被忽略，而
半输出实参则会被考虑在内。

每个候选解决方案都会被保存进一个表中；
这可以防止在回环存在的情况下出现无限回溯，
也可以防止在菱形存在的情况下（即同一目标可通过多条路径实现）出现指数级的搜索开销。
搜索分支在以下任一情况发生时会失败：

- 所有潜在的类实例都已被尝试过，并且搜索空间已被耗尽；

- 达到选项 `synthInstance.maxSize` 所指定的类实例大小上限；

- 输出实参的合成值与
  搜索问题中所指定的值不匹配。
  失败的分支不会被重试。

如果搜索失败或卡住，
那么搜索过程会尝试按照类默认实例优先级顺序来匹配类的默认实例。
对于类的默认实例而言，输入实参
  不需要完全已知，并且
  可能通过实例的实参值进行实例化。
类的默认实例也可能带有实例隐式参数，
这会引入进一步的递归搜索。

在成功的分支中实例搜索问题是完全已知的（即不存在未解决的元变量），
因此这些分支会被剪枝，并且后续的潜在成功类实例也不会被尝试，
因为没有后续类实例能够导致先前成功的分支失败。  

### 10.3.2. 类实例搜索问题 Instance Search Problems {#S10-3-2}
{{< ctx level="3" >}}

类实例搜索可能会在（可能是零元的）函数项的应用被阐述时发生。
某些隐式形参对应的实参值会被其他形参强制求解，比如
一个隐式的类型实参可能会需要借助后续显式提供的实参的类型来求解。
隐式形参也可能会使用程序中该处的预期类型来求解。
实例隐式实参的搜索可能会用到已找到的隐式实参值，
并且还可能会进一步求解其他参数。

类实例合成以实例隐式形参的类型开始。
这个类型必须是一个类类型构造子应用于零个或多个实参的结果；
这些实参值在搜索开始时可能已知，也可能未知。
如果类类型构造子的某个实参是未知的，
那么搜索过程就不会实例化它 ——
除非对应的形参被[标记为输出形参](https://lean-lang.org/doc/reference/latest/Type-Classes/Instance-Synthesis/#class-output-parameters)，
显式地指明其作为实例合成例程的输出。

搜索可能会成功、失败或者是卡住；
如果一个实参从未知的变为已知的，
那么卡住的搜索可能会被重新被启动，从而使搜索得以继续进行。
如果这种情况一直没有发生，那么卡住的搜索就会变成失败搜索。

{{< labelindex 
  type="例子" 
  summary="类实例搜索跟踪信息打印"
>}}
示范：`Nonempty (Nat ⊕ Empty)`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类实例搜索跟踪信息打印" 
  open=false
>}}
将选项 `trace.Meta.synthInstance` 设置为 `true`
会导致 Lean 输出对类实例合成过程的跟踪信息。
这个跟踪信息可以用来理解类实例合成
  是如何成功的，以及
  为什么会失败。

在这里，我们可以看到 Lean 为了得出类类型 `(Nat ⊕ Empty)` 下
存在元素（具体来说是元素 `Sum.inl 0`）所采取的步骤：
点击 `▶` 可以展开被跟踪的分支，而
点击 `▼` 可以折叠已展开的分支。

```lean {wrapper=false, lineNos=false}
set_option pp.explicit true in
set_option trace.Meta.synthInstance true in
#synth Nonempty (Nat ⊕ Empty)
-- [Meta.synthInstance] ✅️ Nonempty (Sum Nat Empty) ▼
--   [] ✅️ new goal Nonempty (Sum Nat Empty) ▼
--     [instances] #[@instNonemptyOfInhabited, @instNonemptyOfMonad, @Sum.nonemptyLeft, @Sum.nonemptyRight] 
--   [apply] ✅️ apply @Sum.nonemptyRight to Nonempty (Sum Nat Empty) ▼
--     [tryResolve] ✅️ Nonempty (Sum Nat Empty) ≟ Nonempty (Sum Nat Empty) ▼
--       [isDefEq] ✅️ Nonempty (Sum Nat Empty) =?= Nonempty (Sum ?m.2 ?m.3) ▼
--         [] ✅️ Sum Nat Empty =?= Sum ?m.2 ?m.3 ▼
--           [] ✅️ Nat =?= ?m.2 ▼ -- ?m.2 : Type ?u.9
--             [] Nat [nonassignable] =?= ?m.2 [assignable] 
--             [] ✅️ Type ?u.9 =?= Type 
--           [] ✅️ Empty =?= ?m.3 ▼ -- ?m.3 : Type ?u.10
--             [] Empty [nonassignable] =?= ?m.3 [assignable] 
--             [] ✅️ Type ?u.10 =?= Type 
--       [isDefEq] ✅️ ?m.1 =?= @Sum.nonemptyRight Nat Empty ?m.4 ▼
--         [] ?m.1 [assignable] =?= @Sum.nonemptyRight Nat Empty ?m.4 [nonassignable] 
--         [] ✅️ Nonempty (Sum Nat Empty) =?= Nonempty (Sum Nat Empty) 
--     [] ✅️ new goal Nonempty Empty ▼
--       [instances] #[@instNonemptyOfInhabited, @instNonemptyOfMonad] 
--   [apply] ❌️ apply @instNonemptyOfMonad to Nonempty Empty ▼
--     [tryResolve] ❌️ Nonempty Empty ≟ Nonempty (?m.5 ?m.6) ▼
--       [isDefEq] ❌️ Nonempty Empty =?= Nonempty (?m.5 ?m.6) ▼
--         [] ❌️ Empty =?= ?m.5 ?m.6 ▼
--           [] Empty [nonassignable] =?= ?m.5 ?m.6 [assignable] 
--           [foApprox] ?m.5 [?m.6] := Empty 
--           [constApprox] ?m.5 [?m.6] := Empty 
--         [onFailure] ❌️ Nonempty Empty =?= Nonempty (?m.5 ?m.6) 
--         [onFailure] ❌️ Nonempty Empty =?= Nonempty (?m.5 ?m.6) 
--   [apply] ✅️ apply @instNonemptyOfInhabited to Nonempty Empty ▼
--     [tryResolve] ✅️ Nonempty Empty ≟ Nonempty Empty ▼
--       [isDefEq] ✅️ Nonempty Empty =?= Nonempty ?m.5 ▼
--         [] ✅️ Empty =?= ?m.5 ▼
--           [] Empty [nonassignable] =?= ?m.5 [assignable] 
--           [] ✅️ Sort ?u.11 =?= Type 
--       [isDefEq] ✅️ ?m.4 =?= @instNonemptyOfInhabited Empty ?m.6 ▼
--         [] ?m.4 [assignable] =?= @instNonemptyOfInhabited Empty ?m.6 [nonassignable] 
--         [] ✅️ Nonempty Empty =?= Nonempty Empty ▼
--           [] ✅️ Empty =?= Empty 
--     [] ✅️ new goal Inhabited Empty ▼
--       [instances] #[@instInhabitedOfMonad] 
--   [apply] ❌️ apply @instInhabitedOfMonad to Inhabited Empty ▼
--     [tryResolve] ❌️ Inhabited Empty ≟ Inhabited (?m.8 ?m.7) ▼
--       [isDefEq] ❌️ Inhabited Empty =?= Inhabited (?m.8 ?m.7) ▼
--         [] ❌️ Empty =?= ?m.8 ?m.7 ▼
--           [] Empty [nonassignable] =?= ?m.8 ?m.7 [assignable] 
--           [foApprox] ?m.8 [?m.7] := Empty 
--           [constApprox] ?m.8 [?m.7] := Empty 
--         [onFailure] ❌️ Inhabited Empty =?= Inhabited (?m.8 ?m.7) 
--         [onFailure] ❌️ Inhabited Empty =?= Inhabited (?m.8 ?m.7) 
--   [apply] ✅️ apply @Sum.nonemptyLeft to Nonempty (Sum Nat Empty) ▼
--     [tryResolve] ✅️ Nonempty (Sum Nat Empty) ≟ Nonempty (Sum Nat Empty) ▼
--       [isDefEq] ✅️ Nonempty (Sum Nat Empty) =?= Nonempty (Sum ?m.2 ?m.3) ▼
--         [] ✅️ Sum Nat Empty =?= Sum ?m.2 ?m.3 ▼
--           [] ✅️ Nat =?= ?m.2 ▼
--             [] Nat [nonassignable] =?= ?m.2 [assignable] 
--             [] ✅️ Type ?u.7 =?= Type 
--           [] ✅️ Empty =?= ?m.3 ▼
--             [] Empty [nonassignable] =?= ?m.3 [assignable] 
--             [] ✅️ Type ?u.8 =?= Type 
--       [isDefEq] ✅️ ?m.1 =?= @Sum.nonemptyLeft Nat Empty ?m.4 ▼
--         [] ?m.1 [assignable] =?= @Sum.nonemptyLeft Nat Empty ?m.4 [nonassignable] 
--         [] ✅️ Nonempty (Sum Nat Empty) =?= Nonempty (Sum Nat Empty) 
--     [] ✅️ new goal Nonempty Nat ▼
--       [instances] #[@instNonemptyOfInhabited, @instNonemptyOfMonad] 
--   [apply] ❌️ apply @instNonemptyOfMonad to Nonempty Nat ▼
--     [tryResolve] ❌️ Nonempty Nat ≟ Nonempty (?m.5 ?m.6) ▼
--       [isDefEq] ❌️ Nonempty Nat =?= Nonempty (?m.5 ?m.6) ▼
--         [] ❌️ Nat =?= ?m.5 ?m.6 ▼
--           [] Nat [nonassignable] =?= ?m.5 ?m.6 [assignable] 
--           [foApprox] ?m.5 [?m.6] := Nat 
--           [constApprox] ?m.5 [?m.6] := Nat 
--         [onFailure] ❌️ Nonempty Nat =?= Nonempty (?m.5 ?m.6) 
--         [onFailure] ❌️ Nonempty Nat =?= Nonempty (?m.5 ?m.6) 
--   [apply] ✅️ apply @instNonemptyOfInhabited to Nonempty Nat ▼
--     [tryResolve] ✅️ Nonempty Nat ≟ Nonempty Nat ▼
--       [isDefEq] ✅️ Nonempty Nat =?= Nonempty ?m.5 ▼
--         [] ✅️ Nat =?= ?m.5 ▼
--           [] Nat [nonassignable] =?= ?m.5 [assignable] 
--           [] ✅️ Sort ?u.11 =?= Type 
--       [isDefEq] ✅️ ?m.4 =?= @instNonemptyOfInhabited Nat ?m.6 ▼
--         [] ?m.4 [assignable] =?= @instNonemptyOfInhabited Nat ?m.6 [nonassignable] 
--         [] ✅️ Nonempty Nat =?= Nonempty Nat ▼
--           [] ✅️ Nat =?= Nat 
--     [] ✅️ new goal Inhabited Nat ▼
--       [instances] #[@instInhabitedOfMonad, instInhabitedNat] 
--   [apply] ✅️ apply instInhabitedNat to Inhabited Nat ▼
--     [tryResolve] ✅️ Inhabited Nat ≟ Inhabited Nat ▼
--       [isDefEq] ✅️ Inhabited Nat =?= Inhabited Nat ▼
--         [] ✅️ Nat =?= Nat 
--       [isDefEq] ✅️ ?m.6 =?= instInhabitedNat ▼
--         [] ?m.6 [assignable] =?= instInhabitedNat [nonassignable] 
--         [] ✅️ Inhabited Nat =?= Inhabited Nat ▼
--           [] ✅️ Nat =?= Nat 
--     [answer] ✅️ Inhabited Nat 
--   [isDefEq] ✅️ ?m.6 =?= instInhabitedNat ▼
--     [] ?m.6 [assignable] =?= instInhabitedNat [nonassignable] 
--     [] ✅️ Inhabited Nat =?= Inhabited Nat ▼
--       [] ✅️ Nat =?= Nat 
--   [resume] ✅️ propagating Inhabited Nat to subgoal Inhabited Nat of Nonempty Nat ▼
--     [] size: 1 
--     [answer] ✅️ Nonempty Nat 
--   [isDefEq] ✅️ ?m.4 =?= @instNonemptyOfInhabited Nat instInhabitedNat ▼
--     [] ?m.4 [assignable] =?= @instNonemptyOfInhabited Nat instInhabitedNat [nonassignable] 
--     [] ✅️ Nonempty Nat =?= Nonempty Nat ▼
--       [] ✅️ Nat =?= Nat 
--   [resume] ✅️ propagating Nonempty Nat to subgoal Nonempty Nat of Nonempty (Sum Nat Empty) ▼
--     [] size: 2 
--     [answer] ✅️ Nonempty (Sum Nat Empty) 
--   [isDefEq] ✅️ Nonempty (Sum Nat Empty) =?= Nonempty (Sum Nat Empty) 
--   [isDefEq] ✅️ Type =?= Type 
--   [isDefEq] ✅️ Type =?= Type 
--   [isDefEq] ✅️ Type =?= Type 
--   [isDefEq] ✅️ Inhabited Nat =?= Inhabited Nat 
--   [isDefEq] ✅️ Nonempty Nat =?= Nonempty Nat 
--   [] result @Sum.nonemptyLeft Nat Empty (@instNonemptyOfInhabited Nat instInhabitedNat) 
```

通过探索跟踪信息，可以发现 Lean
是通过深度优先的回溯搜索来进行类实例搜索的。
要熟悉这一切可能需要一些练习！在上面的例子中，Lean 遵循了以下步骤：

- Lean 首先考虑目标 `Nonempty (Sum Nat Empty)`。
  它看到满足这个目标有四种可能的方式：

  - 实例 `Sum.nonemptyRight`，
    它会创建一个子目标 `Nonempty Empty`。

  - 实例 `Sum.nonemptyLeft`，
    它会创建一个子目标 `Nonempty Nat`。

  - 实例 `instNonemptyOfMonad`， 
    它会创建两个子目标 `Monad (Sum Nat)` 和 `Nonempty Nat`。

  - 实例 `instNonemptyOfInhabited`，
    它会创建一个子目标 `Inhabited (Sum Nat Empty)`。

- Lean 
  应用 `Sum.nonemptyRight` 并
  成功，留下了一个新的目标：`Nonempty Empty`。

- 第一个子目标 `Nonempty Empty` 被考虑。
  Lean 看到满足这个目标有两种可能的方式：

  - 实例 `instNonemptyOfMonad`，但
    它会被拒绝。它不能被使用，因为类型 `Empty`
    不是一个单子应用于某个类型后的结果。

  - 实例 `instNonemptyOfInhabited`，
    它会创建一个子目标 `Inhabited Empty`。

- 新产生的子目标 `Inhabited Empty` 被考虑。
  Lean 看到满足这个目标只有一种可能的方式，即 `instInhabitedOfMonad`，但
  它被拒绝了。原因和前面一样，因为类型 `Empty`
  不是一个单子应用于某个类型后的结果。

- 此时已经没有剩余的选项来实现原来的第一个子目标。搜索回溯，
  使用实例 `Sum.nonemptyLeft`，它需要一个 `Nonempty Nat` 的实例。
  这个搜索最终成功了，这是通过 `Inhabited Nat` 实例实现的。

最初的第三、第四个原始候选项从未被考虑过。
一旦 `Nonempty Nat` 的搜索成功，
`#synth` 命令就会结束并输出解决方案：

```lean {wrapper=false, lineNos=false}
-- @Sum.nonemptyLeft Nat Empty (@instNonemptyOfInhabited Nat instInhabitedNat)
```
{{< /admonition >}}

### 10.3.3. 候选类实例 Candidate Instances {#S10-3-3}
{{< ctx level="3" >}}

在类实例搜索过程中，局部和全局类实例都会被类实例合成所使用。
局部类实例是那些在局部上下文中可用的类实例；它们要么是
  函数的形参，不然就是
  使用 `let` 局部声明的常量。
局部类实例不需要被特别标记，任何类型为类类型的局部变量都会是类实例合成的候选项；
全局类实例是那些在全局环境中可用的类实例；每个全局类实例都是一个已声明的名称，并且
应用了 `instance` 属性。

> 由 `instance` 命令创建的声明会自动应用 `instance` 属性。

{{< labelindex 
  type="例子" 
  summary="类实例搜索采纳局部类实例"
>}}
示范：`Add`，`NatPair`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类实例搜索采纳局部类实例" 
  open=false
>}}
在下述例子中，`addPairs` 包含了一个类型为 `Add NatPair` 的局部类实例：

```lean {wrapper=false, lineNos=false}
set_option trace.Meta.synthInstance true in
def addPairs (p1 p2 : NatPair) : NatPair :=
  let _ : Add NatPair := ⟨fun ⟨x1, y1⟩ ⟨x2, y2⟩ => ⟨x1 + x2, y1 + y2⟩⟩
-- [Meta.synthInstance] ✅️ HAdd Nat Nat Nat ▼ -- 这里对应的是 x1 + x2
--   [] ✅️ new goal HAdd Nat Nat _tc.1 ▼ -- 这个 _tc.1 是一个输出形参
--     [instances] #[
--       @instHAdd
--     ]
--   [apply] ✅️ apply @instHAdd to HAdd Nat Nat Nat ▼
--     [tryResolve] ✅️ HAdd Nat Nat Nat ≟ HAdd Nat Nat Nat
--     [] ✅️ new goal Add Nat ▼
--       [instances] #[
--         @Lean.Grind.AddCommMonoid.toAdd,
--         @Lean.Grind.Semiring.toAdd,
--         instAddNat -- instAddNat : Add Nat
--       ]
--   [apply] ✅️ apply instAddNat to Add Nat ▼
--     [tryResolve] ✅️ Add Nat ≟ Add Nat
--     [answer] ✅️ Add Nat
--   [resume] ✅️ propagating Add Nat to subgoal Add Nat of HAdd Nat Nat Nat ▼
--     [] size: 1
--     [answer] ✅️ HAdd Nat Nat Nat
--   [] result instHAdd
  p1 + p2
-- [Meta.synthInstance] ✅️ HAdd NatPair NatPair NatPair ▼
--   [] ✅️ new goal HAdd NatPair NatPair _tc.1 ▼
--     [instances] #[
--       @instHAdd -- instHAdd.{u_1} {α : Type u_1} [Add α] : HAdd α α α
--     ]
--   [apply] ✅️ apply @instHAdd to HAdd NatPair NatPair NatPair ▼
--     [tryResolve] ✅️ HAdd NatPair NatPair NatPair ≟ HAdd NatPair NatPair NatPair
--     [] ✅️ new goal Add NatPair ▼
--       [instances] #[
--         @Lean.Grind.AddCommMonoid.toAdd,
--         @Lean.Grind.Semiring.toAdd,
--         x✝ -- 这个就是 let 声明的 Add NatPair 类实例
--        ]
--   [apply] ✅️ apply x✝ to Add NatPair ▼
--     [tryResolve] ✅️ Add NatPair ≟ Add NatPair
--     [answer] ✅️ Add NatPair
--   [resume] ✅️ propagating Add NatPair to subgoal Add NatPair of HAdd NatPair NatPair NatPair ▼
--     [] size: 1
--     [answer] ✅️ HAdd NatPair NatPair NatPair
--   [] result instHAdd
```

局部类实例被类实例合成所找到，并被用于加法运算中。
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="类实例搜索会优先考虑局部类实例"
>}}
示范：`Add`，`NatPair`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类实例搜索会优先考虑局部类实例" 
  open=false
>}}
在此处的例子中，尽管已存在一个类型为 `Add NatPair` 的全局类实例，
但在 `addPairs` 内仍然包含一个局部定义的 `Add NatPair` 实例：

```lean {wrapper=false, lineNos=false}
structure NatPair where
  x : Nat
  y : Nat

instance : Add NatPair where
  add
    | ⟨x1, y1⟩, ⟨x2, y2⟩ => ⟨x1 + x2, y1 + y2⟩

def addPairs (p1 p2 : NatPair) : NatPair :=
  let _ : Add NatPair := ⟨fun _ _ => ⟨0, 0⟩⟩
  p1 + p2
```

局部类实例而非全局类实例会被选中。

```lean {wrapper=false, lineNos=false}
#eval addPairs ⟨1, 2⟩ ⟨5, 2⟩
-- { x := 0, y := 0 }
```
{{< /admonition >}}

### 10.3.4. 类实例形参与类实例合成 Instance Parameters and Synthesis {#S10-3-4}
{{< ctx level="3" >}}

类实例搜索过程主要由类类型构造子的形参所控制。
类类型构造子会接受一定数量的形参，并且在实例搜索中，
如果某个类实例对这些形参所做出的选择能够与
正在被合成类实例的类类型构造子的形参相**兼容 Compatible**，
那么该类实例便会被尝试。

类实例本身也可能会接受参数，但
类实例的形参在类实例合成中所扮演的角色是非常不同的。
类实例的形参表示的要么是
  可能会被类实例合成实例化的变量，要么是
  在该实例可以被使用之前需要进一步进行的合成工作。
特别地，类实例的形参可能是
显式的、隐式的，或者是实例隐式的。
如果它们是实例隐式的，那么它们会引入进一步的递归的类实例搜索，
而显式或隐式的形参必须通过合一来求解。

{{< labelindex 
  type="例子" 
  summary="类实例的隐式和显式形参"
>}}
示范：`Nonempty (Nat ⊕ Empty)`，`aNonemptySumInstance`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类实例的隐式和显式形参" 
  open=false
>}}
尽管类实例通常会以隐式或实例隐式的方式接受参数，
但是显式参数也可以在实例合成期间被当作隐式参数来进行填充。
在下述例子中，`aNonemptySumInstance` 是通过类实例合成找到的，
它被显式地应用于 `Nat`，这么做是为了使其类型正确。

```lean {wrapper=false, lineNos=false}
instance aNonemptySumInstance -- 模仿前面的 Sum.nonemptyLeft
    (α : Type) {β : Type} [inst : Nonempty α] :
    Nonempty (α ⊕ β) :=
  let ⟨x⟩ := inst
  ⟨.inl x⟩
set_option pp.explicit true in
set_option trace.Meta.synthInstance true in
#synth Nonempty (Nat ⊕ Empty)
-- [Meta.synthInstance] ✅️ Nonempty (Sum Nat Empty) ▼
--   [] ✅️ new goal Nonempty (Sum Nat Empty) ▼
--     [instances] #[
--       @instNonemptyOfInhabited, 
--       @instNonemptyOfMonad, 
--       @Sum.nonemptyLeft, 
--       @Sum.nonemptyRight, 
--       aNonemptySumInstance
--     ] 
--   [apply] ✅️ apply aNonemptySumInstance to Nonempty (Sum Nat Empty) ▼
--     [tryResolve] ✅️ Nonempty (Sum Nat Empty) ≟ Nonempty (Sum Nat Empty) 
--     [] ✅️ new goal Nonempty Nat ▼
--       [instances] #[
--         @instNonemptyOfInhabited, 
--         @instNonemptyOfMonad
--       ] 
--   [apply] ❌️ apply @instNonemptyOfMonad to Nonempty Nat ▼
--     [tryResolve] ❌️ Nonempty Nat ≟ Nonempty (?m.5 ?m.6) 
--   [apply] ✅️ apply @instNonemptyOfInhabited to Nonempty Nat ▼
--     [tryResolve] ✅️ Nonempty Nat ≟ Nonempty Nat 
--     [] ✅️ new goal Inhabited Nat ▼
--       [instances] #[
--         @instInhabitedOfMonad, 
--         instInhabitedNat
--       ] 
--   [apply] ✅️ apply instInhabitedNat to Inhabited Nat ▼
--     [tryResolve] ✅️ Inhabited Nat ≟ Inhabited Nat 
--     [answer] ✅️ Inhabited Nat 
--   [resume] ✅️ propagating Inhabited Nat to subgoal Inhabited Nat of Nonempty Nat ▼
--     [] size: 1 
--     [answer] ✅️ Nonempty Nat 
--   [resume] ✅️ propagating Nonempty Nat to subgoal Nonempty Nat of Nonempty (Sum Nat Empty) ▼
--     [] size: 2 
--     [answer] ✅️ Nonempty (Sum Nat Empty) 
--   [] result @aNonemptySumInstance Nat Empty (@instNonemptyOfInhabited Nat instInhabitedNat) 
```

在输出中，显式参数 `Nat` 和隐式参数 `Empty`
都是通过与搜索目标进行合一来找到的，
而 `Nonempty Nat` 类实例
则是通过递归的类实例合成来找到的。
{{< /admonition >}}

### 10.3.5. 类类型构造子的输出形参 Output Parameters {#S10-3-5}
{{< ctx level="3" >}}

默认情况下，类类型构造子的形参会被认为是搜索过程的输入。
如果这些形参是未知的，那么搜索过程就会卡住；
因为选出一个类实例要求这些形参对应的实参值
能够与类实例中的值相匹配，
而这些值无法通过不完整的信息来确定。
在大多数情况下，猜测类实例会使得类实例合成变得不可预测。

但在某些情况下，对一个形参做出选择
应该会自动导致对另一个形参做出选择。例如，
类 `Membership` 用于表示重载的成员判断谓词，
其会将数据结构中的元素的类型视为输出；如此一来，
利用调用处数据结构的类型我们便可确定元素的类型。
我们无需再在类实例合成开始前提供充足的类型注释
以确定两种类型。仅需知道一个元素属于 `List Nat`，
便可得知其类型为 `Nat`。

类类型的形参可以通过将它们的类型包装在 `outParam` 零件中来声明为输出形参。
如果类类型构造子的形参是{{< labelindex 
  type="术语" 
  id_alias="类类型构造子的输出形参"
  title_alias="类类型构造子的输出形参 Output Parameter"
>}}
{{< /labelindex >}}**输出形参 Output Parameter**，
那么类实例合成将不再要求形参是已知的。
事实上任何已有的值都会被完全忽略。
首个与输入形参匹配的实例会被选中，并且
该实例对输出形参的所指定的值将成为输出实参的值。
如果有预先存在的值，
那么在类实例合成结束后它将与被指定的值进行比较：
如果它们不匹配那么就报错。

{{< labelindex 
  type="常量" 
  id_alias="outParam"
>}}
零件，用于将类类型构造子的形参标记为输出形参
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
outParam.{u} (α : Sort u) : Sort u
```

一个零件，用于将类类型构造子的形参标记为输出形参。

举个例子，类 `Membership` 的声明如下：

```lean {wrapper=false, lineNos=false}
class Membership (α : outParam (Type u)) (γ : Type v)
```

每当形如 `Membership ?α ?γ` 的类实例目标出现时，Lean 
都会等到 `?γ` 已知之后才去求解它，随后 Lean
便会运行类实例合成并
利用找到的首个解作来决定 `?α` 的取值。

如此便意味着：在任何形如 `a ∈ s` 的项中，`s` 可能是
`Set α`，`List α`，或者是其他具有成员关系操作的类型，并且
在每一种情况下我们都可以通过查看容器类型来确定“成员”类型 `α`。
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="类实例搜索卡住以及解决办法"
>}}
示范：`Serialize`，`Append`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类实例搜索卡住以及解决办法" 
  open=false
>}}
下述序列化框架提供了一种
将值转换为某种底层存储类型的方式：

```lean {wrapper=false, lineNos=false}
class Serialize (input output : Type) where
  ser : input → output
export Serialize (ser)

instance : Serialize Nat String where
  ser n := toString n

instance [Serialize α γ] [Serialize β γ] [Append γ] :
    Serialize (α × β) γ where
  ser
    | (x, y) => ser x ++ ser y
```

在本例中，输出类型是未知的。类实例合成
无法选择 `Serialize Nat String` 下的类实例，也
无法选择 `Append String` 下的类实例，
因为这将要求将输出类型实例化为 `String`，如此搜索便会卡住：

```lean {wrapper=false, lineNos=false}
example := ser (2, 3)
-- typeclass instance problem is stuck
--   Serialize (Nat × Nat) ?m.5
-- 
-- Note: Lean will not try to resolve this typeclass instance problem 
-- because the second type argument to `Serialize` is a metavariable. 
-- This argument must be fully determined 
-- before Lean will try to resolve the typeclass.
-- 
-- Hint: Adding type annotations and supplying implicit arguments to functions 
-- can give Lean more information for typeclass resolution. For example, 
-- if you have a variable `x` that you intend to be a `Nat`, 
-- but Lean reports it as having an unresolved type like `?m`, 
-- replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
```

正如报错信息所示，解决这个问题的其中一种方法是补充一个预期类型：

```lean {wrapper=false, lineNos=false}
example : String := ser (2, 3)
```

另一种解决办法就是将输出类型标记为输出形参：

```lean {wrapper=false, lineNos=false}
class Serialize (input : Type) (output : outParam Type) where
  ser : input → output
export Serialize (ser)

instance : Serialize Nat String where
  ser n := toString n

instance [Serialize α γ] [Serialize β γ] [Append γ] :
    Serialize (α × β) γ where
  ser
    | (x, y) => ser x ++ ser y
```

现在实例合成可以自由地选择 `Serialize Nat String` 下的类实例，
从而求解 `ser` 的未知隐式输出参数：

```lean {wrapper=false, lineNos=false}
example := ser (2, 3)
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="类类型构造子的输出形参被人为提供对应的实参"
>}}
示范：`OneSmaller`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类类型构造子的输出形参被人为提供对应的实参" 
  open=false
>}}
类 `OneSmaller` 用于表示一种
将某个类型的所有非最大元素集中组织成一个新的类型的方式。
下面的代码中有两个不同的类实例可以匹配输入类型 `Option Bool`，
但是它们的输出类型却不相同：

```lean {wrapper=false, lineNos=false}
class OneSmaller (α : Type) (β : outParam Type) where
  biggest : α
  shrink : (x : α) → x ≠ biggest → β

instance : OneSmaller (Option α) α where
  biggest := none
  shrink
    | some x, _ => x

instance : OneSmaller (Option Bool) (Option Unit) where
  biggest := some true
  shrink
    | none, _ => none
    | some false, _ => some ()

instance : OneSmaller Bool Unit where
  biggest := true
  shrink
    | false, _ => ()
```

由于类实例合成会选择最近声明的那个类实例，
因此下面的代码会产生报错：

```lean {wrapper=false, lineNos=false}
set_option trace.Meta.synthInstance true in
#check OneSmaller.shrink (β := Bool) (some false) sorry
-- failed to synthesize instance of type class
--   OneSmaller (Option Bool) Bool
-- 
-- Hint: Type class instance resolution failures 
-- can be inspected with the 
-- `set_option trace.Meta.synthInstance true` command.

-- [Meta.synthInstance] ❌️ OneSmaller (Option Bool) Bool ▼
--   [] ✅️ new goal OneSmaller (Option Bool) _tc.0 ▼ -- 这个 _tc.0 是一个输出形参
--     [instances] #[
--       @instOneSmallerOption, 
--       instOneSmallerOptionBoolUnit
--     ] 
--   [apply] ✅️ apply instOneSmallerOptionBoolUnit to OneSmaller (Option Bool) (Option Unit) ▼
--     [tryResolve] ✅️ OneSmaller (Option Bool) (Option Unit) ≟ OneSmaller (Option Bool) (Option Unit) 
--     [answer] ✅️ OneSmaller (Option Bool) (Option Unit) 
--   [] ❌️ result type
--         OneSmaller (Option Bool) (Option Unit)
--       is not definitionally equal to
--         OneSmaller (Option Bool) Bool 
--   [] result <not-available> 
```

类实例合成会选中 `OneSmaller (Option Bool) (Option Unit)` 下的类实例，
但是却不会将 `β` 的值用于类实例合成。
{{< /admonition >}}

{{< labelindex 
  type="术语" 
  id_alias="类类型构造子的半输出形参"
  title_alias="类类型构造子的半输出形参 Semi-Output Parameter"
>}}
{{< /labelindex >}}**半输出形参 Semi-Output Parameter** 与输出形参类似，
都不要求对应的实参值在合成开始前就已知。与输出形参有所不同的是，
人为提供的半输出实参值在选择类实例时会被考虑在内。

{{< labelindex 
  type="常量" 
  id_alias="semiOutParam"
>}}
零件，用于将类类型构造子的形参标记为半输出形参
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
一个零件，用于将类类型构造子的形参标记为半输出形参。

半输出形参会影响类实例的实参被处理的顺序。Lean 会确定一个顺序，
确保在尝试合成某个实例隐式实参之前，该实例隐式实参类型注解中的
所有非（半）输出实参值都必须已被确定（意味着这些实参值不能包含
任何在类实例合成期间创建的可被赋值的元变量）。这排除了诸如
`instance [Mul β] : Add α where` 这样的类实例
（因为 `β` 可以是任意类型）。
将一个类类型构造子的形参标记为半输出的，
相当于是保证了类实例总是会为该形参提供一个对应的值。

举个例子，`Coe` 类的声明如下：

```lean {wrapper=false, lineNos=false}
class Coe (α : semiOutParam (Sort u)) (β : Sort v)
```

这意味着所有类 `Coe` 的实例都应该为 `α` 提供一个具体的值（即不是一个可被赋值的元变量）。
像 `Coe Nat Int` 或 `Coe α (Option α)` 这样的类实例是合适的，
而 `Coe α Nat` 就不合适，因为它没有为 `α` 提供一个具体的值。
{{< /admonition >}}

半输出形参对类实例施加了一项要求：
对于带有半输出形参的类类型构造子，
每个类实例都应该为其半输出实参提供一个具体的值。

{{< labelindex 
  type="例子" 
  summary="类类型构造子的半输出形参被人为提供对应的实参"
>}}
示范：`OneSmaller`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类类型构造子的半输出形参已被人为提供对应的实参" 
  open=false
>}}
类 `OneSmaller` 用于表示一种
将某个类型的所有非最大元素集中组织成一个新的类型的方式。
该类拥有两个独立的实例，它们
都可以匹配输入类型 `Option Bool`，但是输出类型却不同：

```lean {wrapper=false, lineNos=false}
class OneSmaller (α : Type) (β : semiOutParam Type) where
  biggest : α
  shrink : (x : α) → x ≠ biggest → β

instance : OneSmaller (Option α) α where
  biggest := none
  shrink
    | some x, _ => x

instance : OneSmaller (Option Bool) (Option Unit) where
  biggest := some true
  shrink
    | none, _ => none
    | some false, _ => some ()

instance : OneSmaller Bool Unit where
  biggest := true
  shrink
    | false, _ => ()
```

由于类实例合成在选择类实例时会考虑半输出形参，因此在提供了 `β` 的值之后，
`OneSmaller (Option Bool) (Option Unit)` 就不再是一个可行的候选类实例了。

```lean {wrapper=false, lineNos=false}
set_option trace.Meta.synthInstance true in
#check OneSmaller.shrink (β := Bool) (some false) sorry
-- [Meta.synthInstance] ✅️ OneSmaller (Option Bool) Bool ▼
--   [] ✅️ new goal OneSmaller (Option Bool) Bool ▼
--     [instances] #[@instOneSmallerOption] 
--   [apply] ✅️ apply @instOneSmallerOption to OneSmaller (Option Bool) Bool ▼
--     [tryResolve] ✅️ OneSmaller (Option Bool) Bool ≟ OneSmaller (Option Bool) Bool 
--     [answer] ✅️ OneSmaller (Option Bool) Bool 
--   [] result instOneSmallerOption 
```
{{< /admonition >}}

### 10.3.6. 类默认实例 Default Instances {#S10-3-6}
{{< ctx level="3" >}}

当类实例合成由于没办法选中实例即将失败时，
Lean 会按照类实例优先级尝试使用 `default_instance` 属性
所指定的{{< labelindex 
  type="术语" 
  id_alias="类默认实例"
  title_alias="类默认实例 Default Instance"
>}}
{{< /labelindex >}}**类默认实例 Default Instance**。
在类默认实例优先级相同的情况下，
最新定义的类默认实例会优先于较早定义的类默认实例。
首个能够使搜索成功的类默认实例会被选中。

如果类的默认实例本身具有实例隐式形参，
那么类的默认实例可能会引起进一步的递归类实例搜索。
如果递归搜索失败，那么搜索过程会回溯并尝试下一个类的默认实例。

### 10.3.7. “实质上典范的”类实例 “Morally Canonical” Instances {#S10-3-7}
{{< ctx level="3" >}}

在类实例合成期间，
如果一个目标是完全已知的（也就是说其不包含任何元变量）
并且类实例搜索成功了，
那么对于同一个目标后续的类实例将不会被尝试。换句话说，
如果针对某个目标的搜索成功了，
并且这种成功无法再被后续补充的信息所推翻，
那么即便还存在其他可能可用的类实例，该目标也不会再被尝试。
此优化方案可以预防类实例合成搜索后续分支失败所引起的虚假回溯，
后者会导致源自早期分支的快速解被替换为对大状态空间的缓慢探索。

此优化依赖于{{< labelindex 
  type="术语" 
  id_alias="类实例是实质上典范的"
  title_alias="类实例是实质上典范的 Morally Canonical"
>}}
{{< /labelindex >}}类实例是“**实质上典范的 Morally Canonical**”这一假设。即便是
  给定类的重载操作存在多种潜在的实现方式，或者即便是
  由于菱形而存在多种合成类实例的方式，
任何被发现的类实例都应该被认为与其他类实例一样好。换句话说，
只要当中有一个类实例能被保证是可用的，
那么其他潜在的类实例就没有必要被考虑。
该优化方案可以通过向后兼容选项 `backward.synthInstance.canonInstances` 来禁用。
该选项可能会在 Lean 的未来版本中被移除。

使用实例隐式参数书写代码的程序员应该有将所有类实例都视为彼此等价的觉悟。换句话说，
代码应该能在合成出的类实例的差异面前够保持稳健性。
当代码所依赖的类实例实际上是彼此等价的时，它要么应该
  显式地操作类实例（比如
  通过局部定义将类实例保存在结构字段中，或者是
  让一个结构继承自适当的类），要么应该
  在类型中明确地表达这种依赖关系（使得
  选择不同的类实例会导致不兼容的类型）。

### 10.3.8. 包装合成出的类实例 Wrapping Synthesized Instances {#S10-3-8}
{{< ctx level="3" >}}

在 `inferInstanceAs` 或默认的 `deriving` 处理器合成出一个类实例之后，
类实例声明的主体会被处理，以确保该类实例的类型及其字段的类型能够与
`instances` 透明度下的预期类型相匹配。`instances` 透明度
只会展开可约的和隐式可约的常量声明，这种处理方式可以预防
类实例在其透明度被降低到半可约以下时泄露其定义的内部细节，
后者可能会导致代码库的不同部分之间出现预料之外的依赖关系。

如果预期类型只是一个命题，
那么该类实例会被包装在一个辅助定理声明当中；
否则合成出的类实例在 `instances` 透明度下
会被归约为{{< labelindex 
  type="术语" 
  id_alias="弱头规范形式"
  title_alias="弱头规范形式 Weaked Head Normal Form"
>}}
{{< /labelindex >}}**弱头规范形式 Weaked Head Normal Form**。
如果结果是一个归纳项构造子的应用，那么每个字段都会被处理：

- 如果字段是一个子类实例，并且能够为该字段的类型找到一个对应的类实例，
  那么就用这个新合成的类实例作为字段的值。
  如此便可确保该类实例与用户代码自行合成出的类实例是相同的，从而避免以下情况：
  同一个类实例存在多条获取路径（即菱形），并且
  通过不同路径得到的类实例并不是彼此[定义等价的]({{< relref "read-LeanRef-web-Chpt04.md" >}}#术语-项的定义等价性)。
  如果类实例合成无法找到对应的类实例，
  那么该字段会按照此流程被递归地包装。

- 如果字段是一个证明
  并且字段类型与预期类型并不是定义等价的，
  那么字段会被包装在辅助定理中以隐藏类型间的差异。

- 如果字段是一个数据项
  并且字段类型与预期类型并不是定义等价的，
  那么字段会被包装在具有适当可约性的辅助声明当中。

如果类实例的主体无法被归约为归纳项构造子的应用，
并且其类型与预期类型不匹配，
那么它会被包装在一个具有适当可约性的辅助声明当中。

### 10.3.9. 选项 Options {#S10-3-9}
{{< ctx level="3" >}}

{{< labelindex 
  type="选项" 
  id_alias="backward.synthInstance.canonInstances"
  summary="默认为 `true`"
>}}
是否在类实例合成的过程中使用基于“实质上典范的”类实例的优化方案
{{< /labelindex >}}
{{< admonition 
  type=info
  title="选项：`{{< indexprint >}}`" 
>}}
默认值：`true`。

在类实例合成的过程中使用
基于“实质上典范的”类实例的优化方案。
{{< /admonition >}}

{{< labelindex 
  type="选项" 
  id_alias="synthInstance.maxHeartbeats"
  summary="默认为 `20000`"
>}}
设置每个类实例合成问题的最大心跳数
{{< /labelindex >}}
{{< admonition 
  type=info
  title="选项：`{{< indexprint >}}`" 
>}}
默认值：`20000`。

每个类实例合成问题的最大心跳数。
心跳数是（小）内存分配的数量（以千为单位），
`0` 表示没有限制。
{{< /admonition >}}

{{< labelindex 
  type="选项" 
  id_alias="synthInstance.maxSize"
  summary="默认为 `128`"
>}}
设置类实例合成过程中用于构造解的最大实例数目
{{< /labelindex >}}
{{< admonition 
  type=info
  title="选项：`{{< indexprint >}}`" 
>}}
默认值：`128`。

在类实例合成过程中用于构造解的最大实例数目。
{{< /admonition >}}

{{< labelindex 
  type="选项" 
  id_alias="backward.inferInstanceAs.wrap"
  summary="默认为 `true`"
>}}
是否将类实例声明主体包装在 `inferInstanceAs` 和默认的 `deriving` 处理器中
{{< /labelindex >}}
{{< admonition 
  type=info
  title="选项：`{{< indexprint >}}`" 
>}}
默认值：`true`。

将类实例声明主体包装在
`inferInstanceAs` 和
默认的 `deriving` 处理器中。
{{< /admonition >}}

{{< labelindex 
  type="选项" 
  id_alias="backward.inferInstanceAs.wrap.reuseSubInstances"
  summary="默认为 `true`"
>}}
是否在字段为子类实例时复用目标类型的现有实例而非重新包装它们
{{< /labelindex >}}
{{< admonition 
  type=info
  title="选项：`{{< indexprint >}}`" 
>}}
默认值：`true`。

在递归处理子类实例时会
复用目标类型的现有实例而非
重新包装它们。这对于
避免非定义等价的实例构成的菱形是很重要的。
{{< /admonition >}}

{{< labelindex 
  type="选项" 
  id_alias="backward.inferInstanceAs.wrap.instances"
  summary="默认为 `true`"
>}}
是否将不可约类实例包装在辅助声明中
{{< /labelindex >}}
{{< admonition 
  type=info
  title="选项：`{{< indexprint >}}`" 
>}}
默认值：`true`。

将不可约类实例包装在辅助声明中以修正它们的类型。
{{< /admonition >}}

{{< labelindex 
  type="选项" 
  id_alias="backward.inferInstanceAs.wrap.data"
  summary="默认为 `true`"
>}}
是否在字段为不可约项时将它们包装在辅助声明中
{{< /labelindex >}}
{{< admonition 
  type=info
  title="选项：`{{< indexprint >}}`" 
>}}
默认值：`true`。

将数据字段包装在辅助声明中以修正它们的类型。
{{< /admonition >}}

## 10.4. 类实例派生 Deriving Instances {#S10-4}
{{< ctx level="2" >}}

Lean 可以自动生成许多类下的实例，这个过程被称为
{{< labelindex 
  type="术语" 
  id_alias="类实例派生"
  title_alias="类实例派生 Deriving Instance"
>}}
{{< /labelindex >}}**类实例派生 Deriving Instance**。类实例派生
可以在声明类型时触发，也可以作为独立命令触发。

{{< labelindex 
  type="语法" 
  id_alias="归纳声明（类实例派生）"
>}}
`(deriving …)?`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
作为声明新归纳的命令的一部分，
`deriving` 子句指定了一个逗号分隔的类名称列表，
当中的每个类都会被生成对应的类实例：

```lean {wrapper=false, lineNos=false}
optDeriving ::=
    (deriving derivingClass,*)?
```
{{< /admonition >}}

{{< labelindex 
  type="语法" 
  id_alias="类实例派生"
>}}
`deriving instance … for …`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="语法：{{< indexprint >}}" 
>}}
独立的 `deriving` 命令指定了一个逗号分隔的类名称列表和一个逗号分隔的目标名称列表。
每个指定的类都会为每个指定的目标生成对应的类实例：

```lean {wrapper=false, lineNos=false}
command ::= ...
  | deriving instance derivingClass,* for term,*
```
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="类实例派生自多个归纳类型"
>}}
示范：`BEq`，`Repr`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：类实例派生自多个归纳类型" 
  open=false
>}}
在为多个类利用给定名称派生类实例后（如下方代码所示）：

```lean {wrapper=false, lineNos=false}
structure A where
structure B where

deriving instance BEq, Repr for A, B
```

各个名称都有对应的类实例，因此
所有四个 `#synth` 命令都会成功：

```lean {wrapper=false, lineNos=false}
#synth BEq A
#synth BEq B
#synth Repr A
#synth Repr B
```
{{< /admonition >}}

### 10.4.1. 类实例派生处理器 Deriving Handlers {#S10-4-1}
{{< ctx level="3" >}}

类实例派生会用到一个{{< labelindex 
  type="术语" 
  id_alias="类实例派生处理器"
  title_alias="类实例派生处理器 Deriving Handler"
>}}
{{< /labelindex >}}**类实例派生处理器 Deriving Handler** 表，
它会将类名称映射到用于派生类实例的元程序。
派生处理器可通过 `registerDerivingHandler` 以被添加到表中，
后者应该在 `initialize` 块中被调用。
每个派生处理器的类型都应该是
`Array Name → CommandElabM Bool`。
如果用户请求派生某个类的实例，
那么该类被注册的类实例派生处理器就会被一个接一个地调用。
这些派生处理器会被提供一个数组，数组种包含了
需要被派生类实例的互递归块中的所有名称；并且
这些派生处理器要么
  应正确地派生出一个类实例并返回 `true`，要么
  就不做任何处理并返回 `false`。
如果一个派生处理器返回了 `true`，
那么后续的派生处理器将不会被调用。

Lean 为以下类提供了派生处理器：

-  `BEq`

-  `DecidableEq`

-  `Hashable`

-  `Inhabited`

-  `LawfulBEq`

-  `Nonempty`

-  `Ord`

-  `ReflBEq`

-  `Repr`

-  `SizeOf`

-  `TypeName`

{{< labelindex 
  type="常量" 
  id_alias="Lean.Elab.registerDerivingHandler"
>}}
为一个类注册一个类实例派生处理器
{{< /labelindex >}}
{{< admonition 
  type=info
  title="常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
Lean.Elab.registerDerivingHandler 
  (className : Name)
  (handler : DerivingHandler) 
  : IO Unit
```

为一个类注册一个类实例派生处理器。
该函数常量应该在 `initialize` 块中被调用。

`DerivingHandler` 接收的是其所处理的所有类型的
完全限定名称 Fully Qualified Name；比方说
`deriving instance Foo Bar, Baz`
就会调用 ``fooHandler #[`Bar, `Baz]``
{{< /admonition >}}

{{< labelindex 
  type="例子" 
  summary="自定义类实例派生处理器"
>}}
示范：`IsEnum`，`Bool`，`deriveIsEnum`
{{< /labelindex >}}
{{< admonition 
  type=example
  title="{{< indexprint >}}：派生处理器" 
  open=false
>}}
`IsEnum` 类下的实例可用于证明某个类型是有限的枚举类型；
这是通过接收一个从该类型出发到某个大小适当的 `Fin` 之间的双射来实现的：

```lean {wrapper=false, lineNos=false}
class IsEnum (α : Type) where
  size : Nat
  toIdx : α → Fin size
  fromIdx : Fin size → α
  to_from_id : ∀ (i : Fin size), toIdx (fromIdx i) = i
  from_to_id : ∀ (x : α), fromIdx (toIdx x) = x
```

对于那些简单的枚举归纳（即归纳项构造子不需要任何实参），
该类的实例具有相当多的重复内容。
`Bool` 对应的类实例就是一个典型的例子：

```lean {wrapper=false, lineNos=false}
instance : IsEnum Bool where
  size := 2
  toIdx
    | false => 0
    | true => 1
  fromIdx
    | 0 => false
    | 1 => true
  to_from_id
    | 0 => rfl
    | 1 => rfl
  from_to_id
    | false => rfl
    | true => rfl
```

通过模仿 `IsEnum Bool` 的实现方式，
派生处理器会以自动地构造各个模式的分支：

```lean {wrapper=false, lineNos=false}
import Lean.Elab

open Lean Elab Parser Term Command

def deriveIsEnum (declNames : Array Name) : CommandElabM Bool := do
  if h : declNames.size = 1 then
    let env ← getEnv
    if let some (.inductInfo ind) := env.find? declNames[0] then
      let mut tos : Array (TSyntax ``matchAlt) := #[]
      let mut froms := #[]
      let mut to_froms := #[]
      let mut from_tos := #[]
      let mut i := 0

      for ctorName in ind.ctors do
        let c := mkIdent ctorName
        let n := Syntax.mkNumLit (toString i)

        tos      := tos.push      (← `(matchAltExpr| | $c => $n))
        from_tos := from_tos.push (← `(matchAltExpr| | $c => rfl))
        froms    := froms.push    (← `(matchAltExpr| | $n => $c))
        to_froms := to_froms.push (← `(matchAltExpr| | $n => rfl))

        i := i + 1

      let cmd ← `(instance : IsEnum $(mkIdent declNames[0]) where
                    size := $(quote ind.ctors.length)
                    toIdx $tos:matchAlt*
                    fromIdx $froms:matchAlt*
                    to_from_id $to_froms:matchAlt*
                    from_to_id $from_tos:matchAlt*)
      elabCommand cmd

      return true
  return false

initialize
  registerDerivingHandler ``IsEnum deriveIsEnum
```
{{< /admonition >}}

## 10.5. 基础类 Basic Classes {#S10-5}
{{< ctx level="2" >}}

为了允许如
  加法或
  数组索引
这样的内置符号被重载，
Lean 提供了不少基础类。

### 10.5.1. 布尔等价性测试 Boolean Equality Tests {#S10-5-1}
{{< ctx level="3" >}}

布尔等价性运算符 `==` 的重载是通过声明 `BEq` 类实例来实现的。
它的伴生类 `Hashable` 则用于为一个类型指定 Hashing 的过程。
如果一个类型同时拥有 `BEq` 和 `Hashable` 类的实例，
那么被计算出的 Hash 值就应该遵循 `BEq` 类的实例：
任何两个被 `BEq.beq` 判定为相等的值都应该始终具有相同的 Hash 值。

{{< labelindex 
  type="类" 
  id_alias="BEq"
>}}
类型被补充布尔等价关系
{{< /labelindex >}}
{{< admonition 
  type=info
  title="类：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
BEq.{u} (α : Type u) : Type u
```

类 `BEq α` 用于为类型 `α` 补充一个
返回布尔值的等价关系，记作 `a == b`。
与 `DecidableEq α`（即 `a = b`）所不同的是，
`BEq α` 的类方法返回值是布尔值而非命题值，并且
它没有要求任何公理，比如自反性，或是与 `=` 保持一致。
它主要用于编程应用。若要保证 `==` 和 `=` 一致，
请参阅 `LawfulBEq`。

通常我们更倾向于将
  “更可变”的项放在左边，并且将
  “更恒定”的项放在右边。

**类实例构造子**

`BEq.mk.{u}`

**类实例方法**

`beq : α → α → Bool`

布尔等价性，记作 `a == b`。

标识符的命名惯例：

- `==` 对应标识符的推荐名称是 `beq`。

{{< /admonition >}}

{{< labelindex 
  type="类" 
  id_alias="Hashable"
>}}
类型认定为可被 Hash 成 `UInt64`
{{< /labelindex >}}
{{< admonition 
  type=info
  title="类：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
Hashable.{u} (α : Sort u) : Sort (max 1 u)
```

可被 Hash 成 `UInt64` 的类型。

**类实例构造子**

`Hashable.mk.{u}`

**类实例方法**

`hash : α → UInt64`

将一个值 Hash 成 `UInt64`。

{{< /admonition >}}

{{< labelindex 
  type="不透明常量" 
  id_alias="mixHash"
>}}
不透明 Hash 混合操作，用于实现积类型的 Hash
{{< /labelindex >}}
{{< admonition 
  type=info
  title="不透明常量：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
mixHash (u₁ u₂ : UInt64) : UInt64
```

一个不透明的 Hash 混合操作，
用于实现积类型的 Hash。
{{< /admonition >}}


{{< labelindex 
  type="类" 
  id_alias="LawfulBEq"
>}}
==TODO==
{{< /labelindex >}}
{{< admonition 
  type=info
  title="类：`{{< indexprint >}}`" 
>}}
```lean {wrapper=false, lineNos=false}
LawfulBEq.{u} (α : Type u) [BEq α] : Prop
```

布尔相等性测试与命题相等性一致。

换句话说：

- `a == b` 蕴含 `a = b`.

- `a == a` 为真.

**类实例构造子**

`LawfulBEq.mk.{u}`

**类实例方法**

`eq_of_beq : ∀ {a b : α}, (a == b) = true → a = b`

如果 `a == b` 求值为 `true`，
那么 `a` 和 `b` 在逻辑上是相等的。

- 若继承自 `ReflBeq α`，则还有

  `rfl : ∀ {a : α}, (a == a) = true`

{{< /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="属性" code_wrap=true >}}

### 例子

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

---

> 作者: [采石场的主人](https://ych817.github.io)  
> URL: https://ych817.github.io/posts/842891a/