翻译-Lean Language Reference-10-类
一个操作具有多态性 Polymorphic 意味着其可被用于多种类型。Lean 当中存在三种多态性：
宇宙多态性， 即声明中的宇宙可以通过多种方式实例化；
参数多态性， 即函数可以以类型作为（隐式）实参， 以便允许单段代码可被用于任何类型；
特设多态性 Ad-hoc Polymorphism， 由类实现，当中被重载的操作对于不同类型可能会有不同的实现。
由于 Lean 不允许对类型分情况分析，
因此不论类型实参如何，多态函数都只会实现一致的操作 —— 比如
List.map 就不会因为列表中元素为 String 或 Nat
而突然采取不同的计算方式。当操作无法只通过“统一”方式实现时，
特设多态操作便派上了用场；一个典型用例便是对算术运算符进行重载，
以使其可用于 Nat、Int、Float 及任何其他具有合理加法概念的类型。
特设多态性也可能会牵扯到多种类型；如在给定集合的指定索引处查找值这个操作
就涉及到了集合的类型、索引的类型以及待提取的集合元素的类型。
一个类 Type Class 描述了
一系列待重载的操作（称为方法 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这样接收函数作为实参的类 可以用来提供带有副作用的程序的特殊语法。 被重载的操作的“类型”实际上是一个类型函数，比如Option、IO或Except。谓词和命题 Predicates and Propositions
Decidable类允许 Lean 自动找到一个命题的判定过程。 这被用作是if表达式的基础，使其可根据任何可判定的命题进行分支。
尽管普通多态声明的实例化往往只需提供合适的实参即可， 但是使用了类重载的运算符的实例化用的却是类实例 Instance， 后者为某组特定的形参定义了具体的重载操作。 这些实例隐式形参 Instance Implicit Parameter用方括号表示。在调用处，Lean 要么 会从可用的候选者中合成 Synthesize 出一个合适的类实例，要么便报错。 由于类实例本身也可能具有类实例形参，因此这个搜索过程可能会是递归的， 并最终产生一个复合的类实例值，该值结合了来自各种类实例的代码。因此， 类实例合成也是一种以类型驱动 Type-Directed 方式构造程序的手段。
下面是一些类的典型用例：
类可以用于表示待重载的操作符，比如 可用于多种类型的数字的算术运算，或者是 可用于多种数据结构的成员判断谓词。 通常来说对于给定类型往往只存在一个典范的操作符 —— 毕竟对
Nat来说加法的定义没有其他合理的替代方案； 但是这并非一个必要属性，如有必要库也可以提供替代类实例。类可以用于表示一个代数结构及其所需的额外结构以及公理。 比如一个表示阿贝尔群的类就可能包含 一个二元运算符、 一个一元逆运算符、 一个幺元，外加上 二元运算符满足结合律和交换律的证明、 幺元之所以能构成幺元的证明、 一元逆运算符在运算符两侧都能产生幺元的证明。 在这里可能不存在一个典范的结构选择， 库可能会提供多种方式来实例化给定的一组公理； 比如整数上就存在着两种同样典范的幺半群结构。
类可以用于表示两个类型之间的关系， 使得它们可以一起以某种新颖的方式为库所使用。 类
Coe被用于表示自动插入的类型强制转换，而 类MonadLift被用于表示将具有某种效应的操作运行在期待另一种效应的语境中的方法。类可以用于表示类型驱动的代码生成框架，当中 各个多态类型的实例都会贡献一部分最终程序的内容。比如 类
Repr会为每个类型定义一个规范化的美化打印器，而 多态类型则会拥有多态的Repr实例。最终 当美化打印在一个已知具体类型的表达式上被调用时 —— 比如List (Nat × (String ⊕ Int))， 生成的美化打印器将会包含从List、Prod、Nat、Sum、String、Int的Repr实例中组装而成的代码。
10.1. 类声明 Class Declarations
类的声明通过 class 关键字来实现。
command ::= ...
| declModifiers
class declId bracketedBinder* (: term)?
(extends (ident : )?term,*)?
where
(declModifiers ident ::)?
structFields
(deriving ident,*)?会声明一个新的类。
class 命令会创建一个新的只有单个归纳项构造子的归纳类型构造子，就如同使用
structure 命令一样。事实上 class 和 structure 的效果几乎是相同的，并且
在两者中可以以相同的方式使用默认值等功能。有关结构继承、字段的默认值等其他功能的更多信息
请见此处。
结构声明与类声明之间的区别如下：
方法而非字段被创建
类声明不会创建以类实例为实参的投影函数；相反， 类声明会创建类实例方法， 每个类实例方法都会将对应的实例用作是实例隐式形参。
父类是实例隐式的
对于那些继承自其他类的类，它们的类实例构造子 会将其父类实例用作是实例隐式形参而非显式形参： 当该类的实例被声明时，类实例合成会被用来寻找那些被继承过来的字段的值。 至于那些不是类的父结构则仍然是底层构造子的显式形参。
父投影函数是由类实例合成生成的
结构项投影会利用继承信息 从子结构项中投影出父结构项。 类用的则是类实例合成：给定一个子类实例，类实例合成会构造父类； 因此，类实例方法不会像项投影函数被添加到子结构那样被添加到子类当中。
归纳会被注册为类
归纳声明后的结果会被注册为一个类，如此便可 为其声明类实例并将该实例用作实例隐式形参。
输出参数和半输出参数会被考虑
尽管零件
outParam和semiOutParam在结构声明中没有意义，但是 在类声明中它们被用来控制类实例搜索。
虽然 deriving 子句被允许用于类定义
以保持类声明和结构声明之间的平行性，
但是实际上它们并不常用，
并且应被视为一个高级特性。
Lean 会拒绝那些类型非类类型的实例隐式形参：
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一个非常小的代数层次结构
既可以全部用结构表示（如下面的 S.Magma、S.Semigroup、S.Monoid）
也可以用结构和类混合表示（如下面的 C1.Monoid）
还可以全部都用类表示（如下面的 C2.Magma、C2.Semigroup、C2.Monoid）：
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 C2S.Monoid 的结构项构造子和
C1.Monoid 的类实例构造子具有相同的签名，这是因为
C1.Monoid 的父结构 S.Semigroup 本身并不是类：
#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 的类实例构造子是相同的；
因为它们都没有继承自其他结构或类。
#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 却会取其父类下的实例作为实例隐式形参。
#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 的父投影来恢复实现。
#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 α类类型构造子的形参可通过零件 Gadget 来标记。
零件是特殊的恒等函数，它会使阐述器以不同的方式来处理一个值。
零件并不会改变一个项的含义，但是
它们可能导致在阐述时的搜索程序中项会以不同的方式被处理。
零件 outParam 和 semiOutParam 会影响类实例合成，
它们在类实例合成有关的那一章节中会被详细介绍。
一个类型不论是否构成类类型都不会影响定义等价性。 即便一个类的类型构造子的实参是一样的， 该类的两个实例也未必是相同的，甚至还可能会有很大的不同。
下述二叉堆插入的实现充满了不少问题：
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 类实例：
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 仍然会选中被指定的类实例。
但这么做确实向读者强调了正确的不变量。
10.1.1. 和类型作为类 Sum Types as Classes
大多数类都遵循一种范式：它们都描述了一组可被重载的类实例方法， 用户可以自由地在这些实例方法中进行选择； 自然地这会被建模为一个积类型，当中的类实例方法便是投影。尽管如此， 有一些类却是和类型：它们要求被合成的实例的接收者 首先检查哪一个可用的类实例构造子会被提供。为了将这些类考虑进去， 类声明也可以包含任意的归纳类型，而不仅仅是作为结构声明的扩展形式而已。
command ::= ...
| declModifiers
class inductive declId optDeclSig where
(| declModifiers ident optDeclSig)*
(deriving ident,*)?归纳类类型就像其他归纳类型一样，只不过它们可能会参与类实例的合成。
一个归纳类的典型例子是 Decidable：在含有自由变量的语境当中，
合成一个类实例就相当于是合成对应的判定过程；但是如果没有自由变量，
那么命题的真值就可以仅通过类实例合成来确定（正如 decide 策略所做的那样）。
10.1.2. 类的缩写 Class Abbreviations
某些情况下，代码库中可能到处都存在着彼此相关联的类。与其重复地写下所有的名称， 不如直接声明一个继承了所有彼此相关联的类且不贡献任何新实例方法的类？然而这个 新声明的类有个缺点：它的实例必须被显式声明。
命令 class abbrev 允许声明类缩写，当中
被创建的名称就是其他一系列类的简写。类缩写在背后
是由一个继承了其他类的类所表示的，此外与其对应的
实例构造子还被额外声明为实例，如此新的类也就可以
只通过实例合成来构造了。
plusTimes1 和 plusTimes2 各自都带有一个隐式实例形参，
分别是 AddMul α 和 AddMul' α：
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 应用到自然数项上：
#eval plusTimes1 2 5 7
-- 37但是 plusTimes2 却导致报错，因为
不存在 AddMul' Nat 实例——至少目前为止还未声明任何类实例：
#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 以及其他所有类型的问题：
instance [Add α] [Mul α] : AddMul' α where
#eval plusTimes2 2 5 7
-- 3710.2. 类实例声明 Instance Declarations
类实例声明的语法和常量声明的语法几乎是一样的，唯一的区别仅在于
关键字 def 被替换为 instance，并且
类实例的名称是可选的：
大部分类实例都是通过 where 来定义各个类实例方法的：
instance ::= ...
| instance ((priority := prio))? declId? declSig where
structInstField*尽管如此，由于类本身是归纳， 因此类实例也可以通过任何具有适当类型的项来构造：
instance ::= ...
| instance ((priority := prio))? declId? declSig :=
term类实例也可以通过分类讨论来声明；然而
除了 Decidable 实例外这个特性很少被使用：
instance ::= ...
| instance ((priority := prio))? declId? declSig
(| term => term)*通常来说，带有显式项的类实例声明包含的内容要么是
对结构项构造子的匿名调用（⟨...⟩），不然就是
在彼此定义等价的类型上调用 inferInstanceAs。
类实例的阐述几乎与普通常量的阐述一致，只不过
还需要注意下面所列的注意事项。
如果没有提供类实例名称，那么一个名称会被自动创建：
这个生成的名称可被引用，但是生成名称所使用的算法
在过去曾发生过变化，并且在未来也可能会发生变化；
因此最好是显式地命名那些将会被直接引用的类实例。
新的类实例在被阐述之后会被注册为类实例搜索的候选者。
为一个名称补充属性 instance 可以用来
将任何其他已声明的名称标记为候选者。
对于下述声明：
structure NatWrapper where
val : Nat
instance : BEq NatWrapper where -- 鼠标悬浮在 instance 上即可看到 instBEqNatWrapper
beq
| ⟨x⟩, ⟨y⟩ => x == y名称 instBEqNatWrapper 即为自动生成的新的类实例。
给定下述结构：
structure NatWrapper where
val : Nat下述各种 BEq 类实例的声明都是彼此等价的：
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⟩除了向环境引入不同的名称之外， 下述声明也是彼此等价的：
@[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⟩10.2.1. 递归类实例 Recursive Instances
在 where 结构项声明语法中定义的函数不可以是递归的。
而由于类实例声明是结构项声明的其中一种形式，
因此类实例方法默认也不可以是递归的。尽管如此，
递归归纳类的实例却非常常见。有一个标准的惯用法可以绕过这个限制：
可以先在类实例声明外声明一个递归函数，
然后再在类实例声明中引用它。按照惯例，
这些递归函数与对应的类实例方法应具有相同的名称，
只不过前者的声明发生在类对应的命名空间中。
提供一个归纳声明 NatTree：
inductive NatTree where
| leaf
| branch (left : NatTree) (val : Nat) (right : NatTree)下述 BEq 的类实例会导致报错，
左（l1 == l2）右（r1 == r2）两处的递归调用都会导致报错：
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：
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接下来我们就可以声明类实例了：
instance : BEq NatTree where
beq := NatTree.beq使用归纳项构造子的匿名调用语法也可以实现同样的效果：
instance : BEq NatTree := ⟨NatTree.beq⟩不仅如此，类实例在其自身的声明中也不可以被用于类实例合成。 只有在被声明之后它们才会被标记为可用于实例合成。在嵌套的归纳类型当中， 如果递归出现的类型正好是某个其他归纳类型构造子的实参， 那么要编写递归函数可能还需要先声明一个类实例。 一个惯用的解决方法是在递归函数的声明主体内先局部声明一个类实例， 这个局部类实例包含了对正在被声明的函数的引用， 如此一来类实例合成便可以正确的类型使用局部语境中的每个绑定。
在下述 NatRoseTree 的声明中，待声明的类型的名称
嵌套出现在另一个归纳类型构造子 Array 的实参中：
inductive NatRoseTree where
| node (val : Nat) (children : Array NatRoseTree)检查 NatRoseTree 下的项的等价性需要检查 Array 的等价性。
但是由于类实例在它们自己的声明中通常是无法被用于实例合成的，
因此下面的常量声明会导致报错 —— 即便 NatRoseTree.beq
是一个递归函数并且其
位于自身声明中的作用域内。
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 实例：
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 绑定的实例。
10.2.2. 归纳类实例 Instances of class inductives
许多类实例具有函数类型： 任何会递归调用类实例搜索的类实例本身就构成一个函数， 具有隐式形参的类实例也是如此。 虽然大多数类实例只会从它们自己的实例形参中投射出类实例方法的实现， 但是归纳类类型的类实例通常会对它们的一个或多个实参进行模式匹配， 从而允许类实例选择适当的类实例构造子。 这是通过普通的 Lean 函数语法来实现的。与其他类实例一样， 正在被讨论的函数在它自身的声明中并不可以被用于类实例合成。
由于 DecidableEq α 是 (a b : α) → Decidable (Eq a b) 的缩写，
因此它的实参可以被直接使用，如下所示：
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归纳 StringList 用于表示字符串的单态列表：
inductive StringList where
| nil
| cons (hd : String) (tl : StringList)在下述声明 DecidableEq 类实例的尝试中，
在阐述第二层的 if 时类实例合成会失败；
这是因为类实例在其自身的声明中并不可用于类实例合成：
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 函数， 因此它可以递归地引用自身显式提供的名称：
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 nofun10.2.3. 类实例优先级 Instance Priorities
类实例可以被赋予优先级 Priority。在类实例合成期间， 那些具有更高优先级的实例会被优先考虑。 有关类实例合成的详细信息请参阅类实例合成一节。
类实例优先级可以是数字：
prio ::=
num如果没有指定优先级，那么优先级的默认值（1000）将被使用：
prio ::= ...
| default在默认值数值粒度太细的时候有三种命名优先级可供选择，
分别对应于 100、500 和 10000。
其中 mid 优先级低于 default。
prio ::= ...
| low
prio ::= ...
| mid
prio ::= ...
| high此外优先级还可以进行加减法运算，
因此 default + 2 是一个有效的优先级，对应于 1002。
prio ::= ...
| (prio)
prio ::= ...
| prio + prio
prio ::= ...
| prio - prio10.2.4. 类默认实例 Default Instances
属性 default_instance 用于指定
在缺乏足够信息来选择类实例的情况下应使用哪个类实例作为默认回退值。
如果没有指定优先级，那么类实例优先级的默认值 default 将会被使用。
default_instanceattr ::= ...
| default_instance prio?OfNat Nat 类的默认实例能够让自然数字面量
在缺乏其他类型信息的情况下被解释为 Nat 类型。
它在 Lean 的标准库中被声明，并且优先级被设置为 100。
考虑下述偶数的表示形式，其中偶数由其自身的一半所表示：
structure Even where
half : Nat下述类实例声明允许数字字面量被用于较小的 Even 值
（类实例搜索的深度限制阻止它们被用于任意大的字面量）：
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：
attribute [default_instance 100] ofNatEven0
attribute [default_instance 100] ofNatEvenPlusTwo
#eval 0
-- { half := 0 }
#eval 34
-- { half := 17 }非偶数数字则仍然会使用 OfNat Nat 作为类实例：
#eval 5
-- 510.2.5. instance 属性 The Instance Attributes
属性 instance 用于将一个声明转变为类实例。和其他属性一样，
它可以被应用于全局、局部，或者是仅在当前命名空间被打开时生效。
instance 命令就是一种会自动应用 instance 属性的常量声明形式。
instance将其所作用于的声明转变为一个类实例。
如果优先级未被提供，那么默认的优先级 default 将会被使用。
attr ::= ...
| instance prio? 10.3. 类实例合成 Instance Synthesis
类实例合成是一个递归的搜索过程：其要么 为给定的类构造出一个实例，要么失败。换句话说， 给定一个被注册为类的东西，类实例合成会尝试构造一个居留于该类类型下的项。 类实例合成遵循可约性： 半可约或 不可约 的常量声明不会被展开， 因此除非是可约的，否则一个被声明的类实例不会被自动视为其展开结果。此外 同一个类类型可能会有多个可能的实例；这种情况下类实例优先级和类实例声明顺序会被用作裁决依据； 按照这个规则，对于一系列具有相同优先级的类实例来说，最近声明的那个会被优先考虑。
这个搜索过程 在菱形 Diamond 存在的情况下是高效的，并且 在回环 Cycle 存在的情况下也不会陷入无限循环。 菱形会在存在多条通向给定目标的路径时出现，而 回环则指的是两个类实例中只要其中一个可以被解决另一个便迎刃而解的情况。 菱形在实践中会经常出现，比如考虑使用类来描述数学概念的情形；而 回环常常会由 Lean 的类型强制转换特性自然产生，比如有限集和有限多重集之间的强制类型转换。
#synth 命令可以用于测试类实例合成，而
inferInstance 和 inferInstanceAs 则可用于在需要类实例的位置合成出一个实例。
带有类型注解的 inferInstance 与 inferInstanceAs 并不等价：
后者会预处理合成的实例
以防止实现细节意外泄漏到接口当中。
inferInstanceinferInstance.{u} {α : Sort u} [i : α] : αinferInstance 会通过类实例合成来合成出一个任意目标类型下的值。
这个函数具有与恒等函数相同的类型签名，只不过
[i : α] 参数上的方括号意味着
它会尝试通过类实例合成来构造这个实参
（若 α 不构成一个类类型则操作失败）。示例：
#check (inferInstance : Inhabited Nat)
-- Inhabited Nat
@[instance_reducible]
def foo : Inhabited (Nat × Nat) := inferInstance
example : foo.default = (default, default) := rflinferInstanceAs«inferInstanceAs».{u} (α : Sort u) [i : α] : αinferInstanceAs α 会合成出一个类型为 α 的类实例，然后
将其调整为符合预期类型 β。β 必须是可以从语境中推断出来的。
例如：
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，并且请在必要时为预期类型提供类型注解。
10.3.1. 类实例搜索概要 Instance Search Summary
一般来说类实例合成是一个会随意回溯的递归搜索过程。类实例合成可能 成功（如果一个类实例项被找到），也可能 失败（如果这样的项无法被找到），或者是 卡住（如果信息不足）。 有关类实例合成算法的详细描述可参考 Selsam, Ullrich, 和 de Moura (2020) 的预印本“Tabled Typeclass Resolution”。 一个类实例搜索问题会在一个类类型构造子应用于具体实参时被引入； 这些实参值可能已知，也可能未知。类实例搜索会 尝试每个局部绑定的、类型为类类型的变量，也会按照类实例优先级和类实例声明的先后顺序 尝试每个已注册的类实例。 如果候选的类实例本身还带有实例隐式形参， 那么它们还会引入后续的的类实例合成任务。
一个类实例搜索问题只有在类类型构造子的所有输入实参都已知的情况下才会被尝试。 如果一个问题还无法被尝试，那么该分支就会卡住； 其他子问题的进展可能会使得该问题变得可解。 在类实例搜索开始时，输出或半输出实参可能是已知的，也可能是未知的。 输出实参在 Lean 检查一个类实例是否匹配类实例搜索问题的时候会被忽略，而 半输出实参则会被考虑在内。
每个候选解决方案都会被保存进一个表中； 这可以防止在回环存在的情况下出现无限回溯， 也可以防止在菱形存在的情况下（即同一目标可通过多条路径实现）出现指数级的搜索开销。 搜索分支在以下任一情况发生时会失败：
所有潜在的类实例都已被尝试过，并且搜索空间已被耗尽；
达到选项
synthInstance.maxSize所指定的类实例大小上限；输出实参的合成值与 搜索问题中所指定的值不匹配。 失败的分支不会被重试。
如果搜索失败或卡住， 那么搜索过程会尝试按照类默认实例优先级顺序来匹配类的默认实例。 对于类的默认实例而言，输入实参 不需要完全已知，并且 可能通过实例的实参值进行实例化。 类的默认实例也可能带有实例隐式参数， 这会引入进一步的递归搜索。
在成功的分支中实例搜索问题是完全已知的（即不存在未解决的元变量）， 因此这些分支会被剪枝，并且后续的潜在成功类实例也不会被尝试， 因为没有后续类实例能够导致先前成功的分支失败。
10.3.2. 类实例搜索问题 Instance Search Problems
类实例搜索可能会在（可能是零元的）函数项的应用被阐述时发生。 某些隐式形参对应的实参值会被其他形参强制求解，比如 一个隐式的类型实参可能会需要借助后续显式提供的实参的类型来求解。 隐式形参也可能会使用程序中该处的预期类型来求解。 实例隐式实参的搜索可能会用到已找到的隐式实参值， 并且还可能会进一步求解其他参数。
类实例合成以实例隐式形参的类型开始。 这个类型必须是一个类类型构造子应用于零个或多个实参的结果； 这些实参值在搜索开始时可能已知，也可能未知。 如果类类型构造子的某个实参是未知的， 那么搜索过程就不会实例化它 —— 除非对应的形参被标记为输出形参， 显式地指明其作为实例合成例程的输出。
搜索可能会成功、失败或者是卡住； 如果一个实参从未知的变为已知的， 那么卡住的搜索可能会被重新被启动，从而使搜索得以继续进行。 如果这种情况一直没有发生，那么卡住的搜索就会变成失败搜索。
将选项 trace.Meta.synthInstance 设置为 true
会导致 Lean 输出对类实例合成过程的跟踪信息。
这个跟踪信息可以用来理解类实例合成
是如何成功的，以及
为什么会失败。
在这里，我们可以看到 Lean 为了得出类类型 (Nat ⊕ Empty) 下
存在元素（具体来说是元素 Sum.inl 0）所采取的步骤：
点击 ▶ 可以展开被跟踪的分支，而
点击 ▼ 可以折叠已展开的分支。
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 命令就会结束并输出解决方案：
-- @Sum.nonemptyLeft Nat Empty (@instNonemptyOfInhabited Nat instInhabitedNat)10.3.3. 候选类实例 Candidate Instances
在类实例搜索过程中，局部和全局类实例都会被类实例合成所使用。
局部类实例是那些在局部上下文中可用的类实例；它们要么是
函数的形参，不然就是
使用 let 局部声明的常量。
局部类实例不需要被特别标记，任何类型为类类型的局部变量都会是类实例合成的候选项；
全局类实例是那些在全局环境中可用的类实例；每个全局类实例都是一个已声明的名称，并且
应用了 instance 属性。
由
instance命令创建的声明会自动应用instance属性。
在下述例子中，addPairs 包含了一个类型为 Add NatPair 的局部类实例：
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局部类实例被类实例合成所找到，并被用于加法运算中。
在此处的例子中，尽管已存在一个类型为 Add NatPair 的全局类实例，
但在 addPairs 内仍然包含一个局部定义的 Add NatPair 实例：
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局部类实例而非全局类实例会被选中。
#eval addPairs ⟨1, 2⟩ ⟨5, 2⟩
-- { x := 0, y := 0 }10.3.4. 类实例形参与类实例合成 Instance Parameters and Synthesis
类实例搜索过程主要由类类型构造子的形参所控制。 类类型构造子会接受一定数量的形参，并且在实例搜索中， 如果某个类实例对这些形参所做出的选择能够与 正在被合成类实例的类类型构造子的形参相兼容 Compatible， 那么该类实例便会被尝试。
类实例本身也可能会接受参数，但 类实例的形参在类实例合成中所扮演的角色是非常不同的。 类实例的形参表示的要么是 可能会被类实例合成实例化的变量，要么是 在该实例可以被使用之前需要进一步进行的合成工作。 特别地，类实例的形参可能是 显式的、隐式的，或者是实例隐式的。 如果它们是实例隐式的，那么它们会引入进一步的递归的类实例搜索， 而显式或隐式的形参必须通过合一来求解。
尽管类实例通常会以隐式或实例隐式的方式接受参数，
但是显式参数也可以在实例合成期间被当作隐式参数来进行填充。
在下述例子中，aNonemptySumInstance 是通过类实例合成找到的，
它被显式地应用于 Nat，这么做是为了使其类型正确。
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 类实例
则是通过递归的类实例合成来找到的。
10.3.5. 类类型构造子的输出形参 Output Parameters
默认情况下，类类型构造子的形参会被认为是搜索过程的输入。 如果这些形参是未知的，那么搜索过程就会卡住； 因为选出一个类实例要求这些形参对应的实参值 能够与类实例中的值相匹配， 而这些值无法通过不完整的信息来确定。 在大多数情况下，猜测类实例会使得类实例合成变得不可预测。
但在某些情况下，对一个形参做出选择
应该会自动导致对另一个形参做出选择。例如，
类 Membership 用于表示重载的成员判断谓词，
其会将数据结构中的元素的类型视为输出；如此一来，
利用调用处数据结构的类型我们便可确定元素的类型。
我们无需再在类实例合成开始前提供充足的类型注释
以确定两种类型。仅需知道一个元素属于 List Nat，
便可得知其类型为 Nat。
类类型的形参可以通过将它们的类型包装在 outParam 零件中来声明为输出形参。
如果类类型构造子的形参是输出形参 Output Parameter，
那么类实例合成将不再要求形参是已知的。
事实上任何已有的值都会被完全忽略。
首个与输入形参匹配的实例会被选中，并且
该实例对输出形参的所指定的值将成为输出实参的值。
如果有预先存在的值，
那么在类实例合成结束后它将与被指定的值进行比较：
如果它们不匹配那么就报错。
outParamoutParam.{u} (α : Sort u) : Sort u一个零件，用于将类类型构造子的形参标记为输出形参。
举个例子，类 Membership 的声明如下：
class Membership (α : outParam (Type u)) (γ : Type v)每当形如 Membership ?α ?γ 的类实例目标出现时，Lean
都会等到 ?γ 已知之后才去求解它，随后 Lean
便会运行类实例合成并
利用找到的首个解作来决定 ?α 的取值。
如此便意味着：在任何形如 a ∈ s 的项中，s 可能是
Set α，List α，或者是其他具有成员关系操作的类型，并且
在每一种情况下我们都可以通过查看容器类型来确定“成员”类型 α。
下述序列化框架提供了一种 将值转换为某种底层存储类型的方式：
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，如此搜索便会卡住：
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.正如报错信息所示，解决这个问题的其中一种方法是补充一个预期类型：
example : String := ser (2, 3)另一种解决办法就是将输出类型标记为输出形参：
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 的未知隐式输出参数：
example := ser (2, 3)类 OneSmaller 用于表示一种
将某个类型的所有非最大元素集中组织成一个新的类型的方式。
下面的代码中有两个不同的类实例可以匹配输入类型 Option Bool，
但是它们的输出类型却不相同：
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, _ => ()由于类实例合成会选择最近声明的那个类实例， 因此下面的代码会产生报错：
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) 下的类实例，
但是却不会将 β 的值用于类实例合成。
半输出形参 Semi-Output Parameter 与输出形参类似， 都不要求对应的实参值在合成开始前就已知。与输出形参有所不同的是， 人为提供的半输出实参值在选择类实例时会被考虑在内。
semiOutParam一个零件，用于将类类型构造子的形参标记为半输出形参。
半输出形参会影响类实例的实参被处理的顺序。Lean 会确定一个顺序，
确保在尝试合成某个实例隐式实参之前，该实例隐式实参类型注解中的
所有非（半）输出实参值都必须已被确定（意味着这些实参值不能包含
任何在类实例合成期间创建的可被赋值的元变量）。这排除了诸如
instance [Mul β] : Add α where 这样的类实例
（因为 β 可以是任意类型）。
将一个类类型构造子的形参标记为半输出的，
相当于是保证了类实例总是会为该形参提供一个对应的值。
举个例子，Coe 类的声明如下：
class Coe (α : semiOutParam (Sort u)) (β : Sort v)这意味着所有类 Coe 的实例都应该为 α 提供一个具体的值（即不是一个可被赋值的元变量）。
像 Coe Nat Int 或 Coe α (Option α) 这样的类实例是合适的，
而 Coe α Nat 就不合适，因为它没有为 α 提供一个具体的值。
半输出形参对类实例施加了一项要求： 对于带有半输出形参的类类型构造子， 每个类实例都应该为其半输出实参提供一个具体的值。
类 OneSmaller 用于表示一种
将某个类型的所有非最大元素集中组织成一个新的类型的方式。
该类拥有两个独立的实例，它们
都可以匹配输入类型 Option Bool，但是输出类型却不同：
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) 就不再是一个可行的候选类实例了。
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 10.3.6. 类默认实例 Default Instances
当类实例合成由于没办法选中实例即将失败时，
Lean 会按照类实例优先级尝试使用 default_instance 属性
所指定的类默认实例 Default Instance。
在类默认实例优先级相同的情况下，
最新定义的类默认实例会优先于较早定义的类默认实例。
首个能够使搜索成功的类默认实例会被选中。
如果类的默认实例本身具有实例隐式形参， 那么类的默认实例可能会引起进一步的递归类实例搜索。 如果递归搜索失败，那么搜索过程会回溯并尝试下一个类的默认实例。
10.3.7. “实质上典范的”类实例 “Morally Canonical” Instances
在类实例合成期间， 如果一个目标是完全已知的（也就是说其不包含任何元变量） 并且类实例搜索成功了， 那么对于同一个目标后续的类实例将不会被尝试。换句话说， 如果针对某个目标的搜索成功了， 并且这种成功无法再被后续补充的信息所推翻， 那么即便还存在其他可能可用的类实例，该目标也不会再被尝试。 此优化方案可以预防类实例合成搜索后续分支失败所引起的虚假回溯， 后者会导致源自早期分支的快速解被替换为对大状态空间的缓慢探索。
此优化依赖于类实例是“实质上典范的 Morally Canonical”这一假设。即便是
给定类的重载操作存在多种潜在的实现方式，或者即便是
由于菱形而存在多种合成类实例的方式，
任何被发现的类实例都应该被认为与其他类实例一样好。换句话说，
只要当中有一个类实例能被保证是可用的，
那么其他潜在的类实例就没有必要被考虑。
该优化方案可以通过向后兼容选项 backward.synthInstance.canonInstances 来禁用。
该选项可能会在 Lean 的未来版本中被移除。
使用实例隐式参数书写代码的程序员应该有将所有类实例都视为彼此等价的觉悟。换句话说， 代码应该能在合成出的类实例的差异面前够保持稳健性。 当代码所依赖的类实例实际上是彼此等价的时，它要么应该 显式地操作类实例（比如 通过局部定义将类实例保存在结构字段中，或者是 让一个结构继承自适当的类），要么应该 在类型中明确地表达这种依赖关系（使得 选择不同的类实例会导致不兼容的类型）。
10.3.8. 包装合成出的类实例 Wrapping Synthesized Instances
在 inferInstanceAs 或默认的 deriving 处理器合成出一个类实例之后，
类实例声明的主体会被处理，以确保该类实例的类型及其字段的类型能够与
instances 透明度下的预期类型相匹配。instances 透明度
只会展开可约的和隐式可约的常量声明，这种处理方式可以预防
类实例在其透明度被降低到半可约以下时泄露其定义的内部细节，
后者可能会导致代码库的不同部分之间出现预料之外的依赖关系。
如果预期类型只是一个命题，
那么该类实例会被包装在一个辅助定理声明当中；
否则合成出的类实例在 instances 透明度下
会被归约为弱头规范形式 Weaked Head Normal Form。
如果结果是一个归纳项构造子的应用，那么每个字段都会被处理：
如果字段是一个子类实例，并且能够为该字段的类型找到一个对应的类实例， 那么就用这个新合成的类实例作为字段的值。 如此便可确保该类实例与用户代码自行合成出的类实例是相同的，从而避免以下情况： 同一个类实例存在多条获取路径（即菱形），并且 通过不同路径得到的类实例并不是彼此定义等价的。 如果类实例合成无法找到对应的类实例， 那么该字段会按照此流程被递归地包装。
如果字段是一个证明 并且字段类型与预期类型并不是定义等价的， 那么字段会被包装在辅助定理中以隐藏类型间的差异。
如果字段是一个数据项 并且字段类型与预期类型并不是定义等价的， 那么字段会被包装在具有适当可约性的辅助声明当中。
如果类实例的主体无法被归约为归纳项构造子的应用， 并且其类型与预期类型不匹配， 那么它会被包装在一个具有适当可约性的辅助声明当中。
10.3.9. 选项 Options
backward.synthInstance.canonInstances默认值：true。
在类实例合成的过程中使用 基于“实质上典范的”类实例的优化方案。
synthInstance.maxHeartbeats默认值：20000。
每个类实例合成问题的最大心跳数。
心跳数是（小）内存分配的数量（以千为单位），
0 表示没有限制。
synthInstance.maxSize默认值：128。
在类实例合成过程中用于构造解的最大实例数目。
backward.inferInstanceAs.wrap默认值：true。
将类实例声明主体包装在
inferInstanceAs 和
默认的 deriving 处理器中。
backward.inferInstanceAs.wrap.reuseSubInstances默认值：true。
在递归处理子类实例时会 复用目标类型的现有实例而非 重新包装它们。这对于 避免非定义等价的实例构成的菱形是很重要的。
backward.inferInstanceAs.wrap.instances默认值：true。
将不可约类实例包装在辅助声明中以修正它们的类型。
backward.inferInstanceAs.wrap.data默认值：true。
将数据字段包装在辅助声明中以修正它们的类型。
10.4. 类实例派生 Deriving Instances
Lean 可以自动生成许多类下的实例，这个过程被称为 类实例派生 Deriving Instance。类实例派生 可以在声明类型时触发，也可以作为独立命令触发。
作为声明新归纳的命令的一部分，
deriving 子句指定了一个逗号分隔的类名称列表，
当中的每个类都会被生成对应的类实例：
optDeriving ::=
(deriving derivingClass,*)?独立的 deriving 命令指定了一个逗号分隔的类名称列表和一个逗号分隔的目标名称列表。
每个指定的类都会为每个指定的目标生成对应的类实例：
command ::= ...
| deriving instance derivingClass,* for term,*在为多个类利用给定名称派生类实例后（如下方代码所示）：
structure A where
structure B where
deriving instance BEq, Repr for A, B各个名称都有对应的类实例，因此
所有四个 #synth 命令都会成功：
#synth BEq A
#synth BEq B
#synth Repr A
#synth Repr B10.4.1. 类实例派生处理器 Deriving Handlers
类实例派生会用到一个类实例派生处理器 Deriving Handler 表，
它会将类名称映射到用于派生类实例的元程序。
派生处理器可通过 registerDerivingHandler 以被添加到表中，
后者应该在 initialize 块中被调用。
每个派生处理器的类型都应该是
Array Name → CommandElabM Bool。
如果用户请求派生某个类的实例，
那么该类被注册的类实例派生处理器就会被一个接一个地调用。
这些派生处理器会被提供一个数组，数组种包含了
需要被派生类实例的互递归块中的所有名称；并且
这些派生处理器要么
应正确地派生出一个类实例并返回 true，要么
就不做任何处理并返回 false。
如果一个派生处理器返回了 true，
那么后续的派生处理器将不会被调用。
Lean 为以下类提供了派生处理器：
BEqDecidableEqHashableInhabitedLawfulBEqNonemptyOrdReflBEqReprSizeOfTypeName
Lean.Elab.registerDerivingHandlerLean.Elab.registerDerivingHandler
(className : Name)
(handler : DerivingHandler)
: IO Unit为一个类注册一个类实例派生处理器。
该函数常量应该在 initialize 块中被调用。
DerivingHandler 接收的是其所处理的所有类型的
完全限定名称 Fully Qualified Name；比方说
deriving instance Foo Bar, Baz
就会调用 fooHandler #[`Bar, `Baz]
IsEnum 类下的实例可用于证明某个类型是有限的枚举类型；
这是通过接收一个从该类型出发到某个大小适当的 Fin 之间的双射来实现的：
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 对应的类实例就是一个典型的例子：
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 的实现方式，
派生处理器会以自动地构造各个模式的分支：
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 deriveIsEnum10.5. 基础类 Basic Classes
为了允许如 加法或 数组索引 这样的内置符号被重载， Lean 提供了不少基础类。
10.5.1. 布尔等价性测试 Boolean Equality Tests
布尔等价性运算符 == 的重载是通过声明 BEq 类实例来实现的。
它的伴生类 Hashable 则用于为一个类型指定 Hashing 的过程。
如果一个类型同时拥有 BEq 和 Hashable 类的实例，
那么被计算出的 Hash 值就应该遵循 BEq 类的实例：
任何两个被 BEq.beq 判定为相等的值都应该始终具有相同的 Hash 值。
BEqBEq.{u} (α : Type u) : Type u类 BEq α 用于为类型 α 补充一个
返回布尔值的等价关系，记作 a == b。
与 DecidableEq α（即 a = b）所不同的是，
BEq α 的类方法返回值是布尔值而非命题值，并且
它没有要求任何公理，比如自反性，或是与 = 保持一致。
它主要用于编程应用。若要保证 == 和 = 一致，
请参阅 LawfulBEq。
通常我们更倾向于将 “更可变”的项放在左边，并且将 “更恒定”的项放在右边。
类实例构造子
BEq.mk.{u}
类实例方法
beq : α → α → Bool
布尔等价性，记作 a == b。
标识符的命名惯例：
==对应标识符的推荐名称是beq。
HashableHashable.{u} (α : Sort u) : Sort (max 1 u)可被 Hash 成 UInt64 的类型。
类实例构造子
Hashable.mk.{u}
类实例方法
hash : α → UInt64
将一个值 Hash 成 UInt64。
mixHashmixHash (u₁ u₂ : UInt64) : UInt64一个不透明的 Hash 混合操作， 用于实现积类型的 Hash。
LawfulBEqLawfulBEq.{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
索引 Index
术语
- 多态性 Polymorphic（见 §10）
- 类 Type Class（见 §10）
- 类类型构造子的半输出形参 Semi-Output Parameter（见 §10-3-5）
- 类类型构造子的输出形参 Output Parameter（见 §10-3-5）
- 类默认实例 Default Instance（见 §10-3-6）
- 类实例 Instance（见 §10）
- 类实例方法 Method（见 §10）
- 类实例合成 Synthesize（见 §10）
- 类实例派生 Deriving Instance（见 §10-4）
- 类实例派生处理器 Deriving Handler（见 §10-4-1）
- 类实例是实质上典范的 Morally Canonical（见 §10-3-7）
- 类实例优先级 Priority（见 §10-2-3）
- 零件 Gadget（见 §10-1）
- 弱头规范形式 Weaked Head Normal Form（见 §10-3-8）
- 实例隐式形参 Instance Implicit Parameter（见 §10）
- 特设多态性 Ad-hoc Polymorphism（见 §10）
语法
常量
inferInstance（见 §10-3）同id但是会使用类实例合成inferInstanceAs（见 §10-3）合成一个类实例并将其调整为符合预期类型outParam（见 §10-3-5）零件，用于将类类型构造子的形参标记为输出形参semiOutParam（见 §10-3-5）零件，用于将类类型构造子的形参标记为半输出形参Lean.Elab.registerDerivingHandler（见 §10-4-1）为一个类注册一个类实例派生处理器
不透明常量
定理
公理
归纳
结构
类
选项
backward.synthInstance.canonInstances： 默认为true（见 §10-3-9）是否在类实例合成的过程中使用基于“实质上典范的”类实例的优化方案synthInstance.maxHeartbeats： 默认为20000（见 §10-3-9）设置每个类实例合成问题的最大心跳数synthInstance.maxSize： 默认为128（见 §10-3-9）设置类实例合成过程中用于构造解的最大实例数目backward.inferInstanceAs.wrap： 默认为true（见 §10-3-9）是否将类实例声明主体包装在inferInstanceAs和默认的deriving处理器中backward.inferInstanceAs.wrap.reuseSubInstances： 默认为true（见 §10-3-9）是否在字段为子类实例时复用目标类型的现有实例而非重新包装它们backward.inferInstanceAs.wrap.instances： 默认为true（见 §10-3-9）是否将不可约类实例包装在辅助声明中backward.inferInstanceAs.wrap.data： 默认为true（见 §10-3-9）是否在字段为不可约项时将它们包装在辅助声明中
属性
default_instance（见 §10-2-4）设置类默认实例及其对应的优先级instance（见 §10-2-5）将常量声明为类实例并指定类实例优先级
例子
- 10-01-例子-01：
只有类才能有实例示范：
def f [n : Nat] : n = n := rfl - 10-01-例子-02：
类实例构造子和结构项构造子的区别示范：
S、C1.Monoid、C2.Magma、C2.Semigroup、C2.Monoid - 10-01-例子-03：
类类型下的实例不唯一所导致的问题示范：
Ord，Heap，Heap' - 10-01-例子-04：
类缩写声明与类声明的区别示范：
Add，Mul，AddMul，AddMul' - 10-02-例子-01：
类实例名称的自动生成示范：
BEq，NatWrapper - 10-02-例子-02：
类实例声明的各种变体示范：
BEq，NatWrapper - 10-02-例子-03：
类实例声明为递归的示范：
BEq，NatTree - 10-02-例子-04：
类实例与嵌套归纳类型有关的情况示范：
BEq，NatRoseTree - 10-02-例子-05：
归纳类的实例示范：
DecidableEq，ThreeChoices - 10-02-例子-06：
归纳类实例声明为递归的示范：
DecidableEq，StringList - 10-02-例子-07：
类默认实例优先级的设置示范：
OfNat，Even - 10-03-例子-01：
类实例搜索跟踪信息打印示范：
Nonempty (Nat ⊕ Empty) - 10-03-例子-02：
类实例搜索采纳局部类实例示范：
Add，NatPair - 10-03-例子-03：
类实例搜索会优先考虑局部类实例示范：
Add，NatPair - 10-03-例子-04：
类实例的隐式和显式形参示范：
Nonempty (Nat ⊕ Empty)，aNonemptySumInstance - 10-03-例子-05：
类实例搜索卡住以及解决办法示范：
Serialize，Append - 10-03-例子-06：
类类型构造子的输出形参被人为提供对应的实参示范：
OneSmaller - 10-03-例子-07：
类类型构造子的半输出形参被人为提供对应的实参示范：
OneSmaller - 10-04-例子-01：
类实例派生自多个归纳类型示范：
BEq，Repr - 10-04-例子-02：
自定义类实例派生处理器示范：
IsEnum，Bool，deriveIsEnum
微信