Lean 中的许多类型类用于让加法、数组索引等内置记法可以重载。
布尔相等运算符 == 通过定义 BEq 的实例来重载。
配套的 Hashable 类为类型指定哈希过程。
当某个类型同时具有 BEq 和 Hashable 实例时，计算出的哈希值应当遵循 BEq 实例：被 BEq.beq 判为相等的两个值应始终具有相同的哈希值。
主要有两种方式为一个类型的值规定次序：
Ord 类型类提供三路比较运算符 compare，它可以指出一个值小于、等于或大于另一个值。它返回一个 Ordering。
LT 和 LE 类为类型提供取值于 Prop 的典范排序关系，且这些关系不必是可判定的。它们用于重载 < 和 ≤ 运算符。
compare 方法已被导出，因此使用它时无需显式写出 Ord 命名空间。
反转一个 Ord 实例的次序。
结果是一个 Ord α 实例：当 ord 返回 Ordering.gt 时它返回 Ordering.lt，
当 ord 返回 Ordering.lt 时它返回 Ordering.gt。
交换小于与大于这两种比较结果。
示例：
若 a 与 b 均为 Ordering，则除非 a 是 .eq，a.then b 都返回 a；当
a 是 .eq 时，它返回 b。此外，它还具有类似布尔运算 && 的“短路”行为：若
a 不是 .eq，则不会求值表达式 b。
这是构造字典序比较函数时很有用的基本操作。对结构体使用 deriving Ord 语法时，
会通过 Ord 实例依次比较各字段，并以等价于 Ordering.then 的方式组合结果。
可使用 compareLex 按字典序组合两个比较函数。
示例：
structure Person where
name : String
age : Nat
-- 先按姓名升序排列；姓名相同时，再按年龄降序排列
instance : Ord Person where
compare a b := (compare a.name b.name).then (compare b.age a.age)
#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Dana", 50⟩
Ordering.gt#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Gert", 50⟩
Ordering.gt#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Gert", 20⟩
Ordering.ltcompareOfLessAndEq.{u_1} {α : Type u_1} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] : OrderingcompareOfLessAndEq.{u_1} {α : Type u_1} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] : Ordering
使用可判定的严格小于关系和相等关系求出一个 Ordering。
具体而言，若 x < y，结果为 Ordering.lt；若 x = y，结果为 Ordering.eq；
否则结果为 Ordering.gt。
compareOfLessAndBEq 使用 BEq 而不是 DecidableEq。
使用可判定的严格小于关系和布尔相等性测试求出一个 Ordering。
具体而言，若 x < y，结果为 Ordering.lt；若 x == y，结果为 Ordering.eq；
否则结果为 Ordering.gt。
compareOfLessAndEq 使用 DecidableEq 而不是 BEq。
compareLex.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (cmp₁ cmp₂ : α → β → Ordering) (a : α) (b : β) : OrderingcompareLex.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (cmp₁ cmp₂ : α → β → Ordering) (a : α) (b : β) : Ordering
使用 cmp₁ 和 cmp₂ 按字典序比较 a 与 b。
首先用 cmp₁ 比较 a 与 b。若其返回 Ordering.eq，则用 cmp₂ 比较
a 与 b，以打破平局。
若要按字典序组合两个 Ordering，请使用 Ordering.then。
小于运算符在 LT 类中重载：
term ::= ...
| 小于关系：`x < y`。
标识符中的记法约定：建议将 `<` 写作 `lt`。
小于等于运算符在 LE 类中重载：
term ::= ...
| 小于等于关系：`x ≤ y`。
标识符中的记法约定：建议将 `≤` 写作 `le`。大于和大于等于运算符分别是小于和小于等于运算符的反向形式，不能独立重载：
term ::= ...
| `a > b` 是 `b < a` 的缩写。
标识符中的记法约定：建议将 `>` 写作 `gt`。term ::= ...
| `a ≥ b` 是 `b ≤ a` 的缩写。
标识符中的记法约定：建议将 `≥` 写作 `ge`。
可以用以下辅助函数从 Ord 构造 BEq、LT 和 LE 实例。
这些辅助函数不会自动成为实例，因为对许多类型而言，自定义关系更为合适。
Ord 实例构造 LT 和 LE 实例
Lean 可以自动派生 Ord 实例。
在本例中，Ord Vegetable 实例按字典序比较蔬菜：
structure Vegetable where
color : String
size : Fin 5
deriving Ord
def broccoli : Vegetable where
color := "green"
size := 2
def sweetPotato : Vegetable where
color := "orange"
size := 3
使用辅助函数 ltOfOrd 和 leOfOrd，可以定义 LT Vegetable 与 LE Vegetable 实例。
这些实例使用 compare 比较蔬菜，并在逻辑上断言结果符合预期。
instance : LT Vegetable := ltOfOrd
instance : LE Vegetable := leOfOrd
所得关系是可判定的，因为 Ordering 上的相等性是可判定的：
#eval broccoli < sweetPotato
#eval broccoli ≤ sweetPotato
#eval broccoli < broccoli
#eval broccoli ≤ broccoli
根据 α 和 β 上的次序，构造积类型 α × β 上的字典序。
按字典序组合两个已有实例，构造一个 Ord 实例。
所得实例先用 ord₁ 比较元素；若其返回 Ordering.eq，再用 ord₂ 比较。
函数 compareLex 可以在不构造中间 Ord 实例的情况下完成这种比较。
Ordering.then 可以按字典序组合各次比较的结果。
类 Max 和 Min 提供重载运算符，用于从两个值中选择较大者或较小者。
若 Ord、LT 和 LE 实例存在，它们应当与这些运算符保持一致，但并没有强制这一点的机制。
给定一个 LE.le 可判定的 LE α 实例，可以使用辅助函数 minOfLe 和 maxOfLe 创建合适的 Min α 与 Max α 实例。
它们可以用作 Lean.Parser.Command.declaration : commandinstance 声明的右侧。
如果一个命题可以通过算法检查，那么它就是可判定的。
排中律意味着每个命题非真即假，但它没有提供检查究竟是哪种情形成立的方法；而这种检查往往很有用。
默认情况下，作用域中只有可生成代码的算法式 Decidable 实例；打开 Classical 命名空间则会使每个命题都可判定。
要么给出命题 p 为真的证明，要么给出命题 p 为假的证明。这等价于一个 Bool，
再配上该 Bool 为 true 当且仅当 p 为真的证明。
Decidable 实例主要通过 if 表达式和 decide 策略使用。在条件表达式中，命题的
Decidable 实例用于选择分支。运行时，这种分类生成的代码与基于 Bool 的条件表达式
所生成的代码相同。在证明中，decide 策略会合成 Decidable p 的实例，尝试将其归约为
isTrue h，若成功便使用证明 h 完成目标。
由于 Decidable 携带数据，在编写左侧包含 Decidable 实例的 @[simp] 引理时，最好使用
{_ : Decidable p} 而不是 [Decidable p]，这样非典范实例可以通过合一找到，而不是通过
实例合成找到。
构造子
Decidable.isFalse {p : Prop} (h : ¬p) : Decidable p
通过提供 ¬p 的证明来证明 p 可判定。
Decidable.isTrue {p : Prop} (h : p) : Decidable p
通过提供 p 的证明来证明 p 可判定。
当命题 p 可判定，并且无论 p 为真还是为假都足以构造 q 时，构造一个 q。
这是依赖式 if-then-else 运算符 dite 的同义形式。
Decidableexample (f g : Nat → Nat) : Decidable (f = g) := inferInstance
打开 Classical 会使每个命题都可判定；不过，使用这一事实的声明和示例必须标记为 Lean.Parser.Command.declaration : commandnoncomputable，以表明不应为它们生成代码。
open Classical
noncomputable example (f g : Nat → Nat) : Decidable (f = g) :=
inferInstance
Inhabited α 是一个类型类，表示 α 有一个指定元素，称为 (default : α)。这种类型有时
称为“居留类型”。
需要在“定义域之外”被调用时仍返回该类型值的函数会使用这个类。例如，若 arr : Array α，
则 Array.get! arr i : α 在 i 越界时会报告 panic；但这不会终止程序，因此函数仍必须返回
一个 α 类型的值（逻辑一致性事实上也要求如此），此时它返回 default。
实例构造子
Inhabited.mk.{u}
方法
default : α
default 生成任意居留类型的“默认”元素。该元素没有任何特别规定的性质，但通常是全零值。
_子单例_是至多有一个元素的类型：它要么为空，要么有唯一元素。
由于证明无关性，所有命题都是子单例：假命题为空，而真命题的任意两个证明彼此相等。 某些非命题类型也是子单例。
实例构造子
Subsingleton.intro.{u}
通过证明任意两个元素相等来证明 α 是子单例。
方法
allEq : ∀ (a b : α), a = b
子单例中的任意两个元素都相等。
如果一个类型是子单例，那么它的所有元素都相等。
异质加法记法的类型类。
它启用记法 a + b : γ，其中 a : α、b : β。
实例构造子
HAdd.mk.{u, v, w}
方法
hAdd : α → β → γ
a + b 计算 a 与 b 的和。该记法的含义取决于类型。
异质减法记法的类型类。
它启用记法 a - b : γ，其中 a : α、b : β。
实例构造子
HSub.mk.{u, v, w}
方法
hSub : α → β → γ
a - b 计算 a 与 b 的差。该记法的含义取决于类型。
对自然数，此运算在 0 处饱和：当 a ≤ b 时，a - b = 0。
异质乘法记法的类型类。
它启用记法 a * b : γ，其中 a : α、b : β。
实例构造子
HMul.mk.{u, v, w}
方法
hMul : α → β → γ
a * b 计算 a 与 b 的积。该记法的含义取决于类型。
标量乘法运算的类型类，记作 •（输入 \bu）。
实例构造子
SMul.mk.{u, v}
方法
smul : M → α → α
m • a : α 表示 m : M 与 a : α 的积。该记法的含义取决于类型，但预期用于左作用。
异质除法记法的类型类。
它启用记法 a / b : γ，其中 a : α、b : β。
实例构造子
HDiv.mk.{u, v, w}
方法
hDiv : α → β → γ
a / b 计算 a 除以 b 的结果。该记法的含义取决于类型。
∣ 运算（输入 \|）的记法类型类；该运算表示整除。
实例构造子
Dvd.mk.{u_1}
方法
dvd : α → α → Prop
整除。a ∣ b（输入 \|）表示存在某个 c，使得 b = a * c。
异质幂运算记法的类型类。
它启用记法 a ^ b : γ，其中 a : α、b : β。
实例构造子
HPow.mk.{u, v, w}
方法
hPow : α → β → γ
a ^ b 计算 a 的 b 次幂。该记法的含义取决于类型。
HPow 的同质版本：a ^ b : α，其中 a : α、b : β。（右参数与左参数类型不必相同，
因为即使在同质情形中也常有这种需求。）
类型可以通过提供 NatPow 或 HomogeneousPow 的实例来选择特定的默认行为：
HomogeneousPow 用于底数和指数优先具有相同类型的类型。
实例构造子
Pow.mk.{u, v}
方法
pow : α → β → α
a ^ b 计算 a 的 b 次幂。参见 HPow。
指数与底数类型相同的完全同质 Pow 版本。此类的用途是提供默认 Pow 实例，使精译过程中
可以将指数特化为与底数相同的类型。也就是说，当 x ^ y 应精译为 x 和 y 具有相同
类型时，该类型应提供此类的实例。
例如，Float 类型提供此类的实例，因此 (2.2 ^ 2.2 : Float) 这样的表达式可以精译。
实例构造子
HomogeneousPow.mk.{u}
方法
pow : α → α → α
a ^ b 计算 a 的 b 次幂，其中 a 和 b 具有相同类型。
HShiftLeft 的同质版本：a <<< b : α，其中 a b : α。
实例构造子
ShiftLeft.mk.{u}
方法
shiftLeft : α → α → α
a <<< b : α 的实现。参见 HShiftLeft。
HShiftRight 的同质版本：a >>> b : α，其中 a b : α。
实例构造子
ShiftRight.mk.{u}
方法
shiftRight : α → α → α
a >>> b : α 的实现。参见 HShiftRight。
a &&& b : γ 记法背后的类型类，其中 a : α、b : β。
实例构造子
HAnd.mk.{u, v, w}
方法
hAnd : α → β → γ
a &&& b 计算 a 与 b 的逐位与。该记法的含义取决于类型。
a ||| b : γ 记法背后的类型类，其中 a : α、b : β。
实例构造子
HOr.mk.{u, v, w}
方法
hOr : α → β → γ
a ||| b 计算 a 与 b 的逐位或。该记法的含义取决于类型。
a ^^^ b : γ 记法背后的类型类，其中 a : α、b : β。
实例构造子
HXor.mk.{u, v, w}
方法
hXor : α → β → γ
a ^^^ b 计算 a 与 b 的逐位异或。该记法的含义取决于类型。
异质追加记法的类型类。
它启用记法 a ++ b : γ，其中 a : α、b : β。
实例构造子
HAppend.mk.{u, v, w}
方法
hAppend : α → β → γ
a ++ b 是 a 与 b 的连接结果，通常读作“追加”。该记法的含义取决于类型。
GetElem.{u, v, w} (coll : Type u) (idx : Type v) (elem : outParam (Type w)) (valid : outParam (coll → idx → Prop)) : Type (max (max u v) w)GetElem.{u, v, w} (coll : Type u) (idx : Type v) (elem : outParam (Type w)) (valid : outParam (coll → idx → Prop)) : Type (max (max u v) w)
GetElem 和 GetElem? 类实现元素查找记法，具体包括 xs[i]、xs[i]?、xs[i]! 和
xs[i]'p。
这两个类都以 coll、idx 和 elem 类型为索引，它们分别是容器、索引和元素类型。
一个容器可以支持使用多种索引类型进行查找。关系 valid 决定索引何时保证有效；有效索引
的查找保证不会失败。
例如，数组的实例形如 GetElem (Array α) Nat α (fun xs i => i < xs.size)。换言之，给定数组
xs 和自然数 i，当 valid xs i 成立时，xs[i] 返回一个 α；这里 valid xs i 在 i
小于数组大小时为真。Array 还支持使用 USize 而非 Nat 索引。无论哪种情况，由于边界
在编译时检查，运行时都不需要检查。
对于 xs[i]（其中 xs : coll 且 i : idx），Lean 会寻找
GetElem coll idx elem valid 的实例，并据此推断返回类型 elem 以及保证 xs[i] 产生有效
elem 值所需的旁条件 valid。系统调用 get_elem_tactic 策略自动证明有效性；xs[i]'p
记法则使用证明 p 满足有效性条件。若证明 p 很长，通常更容易用 have 将其放入上下文，
因为 get_elem_tactic 会尝试 assumption。
证明旁条件 valid xs i 会自动交给 get_elem_tactic；可以用 macro_rules 向
get_elem_tactic_extensible 添加更多分支来扩展该策略。
xs[i]? 和 xs[i]! 不产生证明义务：前者返回 Option elem，以 none 表示值不存在；后者
返回 elem，但在值不存在时会 panic，并根据 Inhabited elem 实例返回 default : elem。
这些操作由 GetElem? 类提供；只要 valid xs i 总是可判定，就可以从 GetElem 类生成默认
实例。
重要实例包括：
arr[i] : α，其中 arr : Array α 且 i : Nat 或 i : USize：执行数组索引，不做运行时
边界检查，并产生证明旁目标 i < arr.size。
l[i] : α，其中 l : List α 且 i : Nat：索引列表，并产生证明旁目标 i < l.length。
实例构造子
GetElem.mk.{u, v, w}
方法
getElem : (xs : coll) → (i : idx) → valid xs i → elem
语法 arr[i] 获取容器 arr 的第 i 个元素。如果应用存在证明旁条件，
get_elem_tactic 策略会自动推断它们。
GetElem?.{u, v, w} (coll : Type u) (idx : Type v) (elem : outParam (Type w)) (valid : outParam (coll → idx → Prop)) : Type (max (max u v) w)GetElem?.{u, v, w} (coll : Type u) (idx : Type v) (elem : outParam (Type w)) (valid : outParam (coll → idx → Prop)) : Type (max (max u v) w)
GetElem 和 GetElem? 类实现元素查找记法，具体包括 xs[i]、xs[i]?、xs[i]! 和
xs[i]'p。容器、索引、元素类型及有效性关系的含义与 GetElem 相同。
实例构造子
GetElem?.mk.{u, v, w}
扩展
LawfulGetElem.{u, v, w} (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) [ge : GetElem? cont idx elem dom] : PropLawfulGetElem.{u, v, w} (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) [ge : GetElem? cont idx elem dom] : Prop
合法的 GetElem? 实例（它扩展 GetElem）应使可能失败的 GetElem?.getElem? 和
GetElem?.getElem! 运算符在有效性谓词成立时成功，在不成立时失败。
实例构造子
LawfulGetElem.mk.{u, v, w}
方法
getElem?_def : ∀ (c : cont) (i : idx) [inst : Decidable (dom c i)], c[i]? = if h : dom c i then some c[i] else none
GetElem?.getElem? 在有效性谓词成立时成功，否则失败。
getElem!_def : ∀ [inst : Inhabited elem] (c : cont) (i : idx), c[i]! = match c[i]? with | some e => e | none => default
GetElem?.getElem! 的成败与 GetElem?.getElem? 的成败一致。