CoeHead α β 用于在强制转换链开头至多应用一次、按从左到右方向进行的强制转换。
实例构造子
CoeHead.mk.{u, v}
方法
coe : α → β
将类型为 α 的值强制转换为类型 β。可通过记法 ↑x 或双重类型标注 ((x : α) : β) 使用。
11.2. 类型间强制转换
当 Lean 精译器成功构造出一个项并推断出其类型，而所在上下文却期望另一种类型的项时，就会插入类型间强制转换。
在报告错误之前，精译器会尝试合成 CoeT 的实例，从而插入从推断类型到预期类型的强制转换。
这一尝试可能通过两种方式成功：
-
可以存在一条经过若干中间类型、从推断类型到预期类型的强制转换链。 这些成链的强制转换根据推断类型和预期类型来选择，而不考虑被强制转换的项。
-
可以存在一个从推断类型到预期类型的依赖强制转换。 依赖强制转换除推断类型和预期类型外，还会考虑被强制转换的项，但它们不能成链。
定义非依赖强制转换最简单的方式是实现一个 Coe 实例，这足以合成一个 CoeT 实例。
此实例会参与成链，并且可以应用任意多次。
合成 Coe 实例由表达式的预期类型而非推断类型驱动。
对于至多只能使用一次的实例，或应由推断类型驱动合成的实例，可能需要使用其他强制转换类之一。
定义强制转换
类型 Even 表示偶自然数。
structure Even where
number : Nat
isEven : number % 2 = 0
强制转换使偶数可用于期望自然数的位置。
coe 属性将该投影标记为强制转换，使其能在证明状态和错误消息中相应显示，具体见实现强制转换一节。
attribute [coe] Even.number
instance : Coe Even Nat where
coe := Even.number
有了这个强制转换，就可以在期望自然数的位置使用偶数。
def four : Even := ⟨4, ⊢ 4 % 2 = 0 All goals completed! 🐙⟩
#eval (four : Nat) + 1
由于强制转换可以成链，将 Coe Even Nat 实例与已有的从 Nat 到 Int 的强制转换连接起来，还会形成一个从 Even 到 Int 的强制转换：
#eval (four : Int) - 5
依赖强制转换用于必须根据被强制转换的具体项来确定能否或如何转换该项的情况：例如，只有可判定命题才能强制转换为 Bool，所以相关命题必须出现在实例类型中，以便该类型能够要求 Decidable 实例。
只要推断类型的所有值都能强制转换为目标类型，就使用非依赖强制转换。
定义依赖强制转换
非依赖强制转换可以成链：如果存在从 α 到 β 的强制转换以及从 β 到 γ 的强制转换，那么也存在从 α 到 γ 的强制转换。
强制转换链应具有 CoeHead?CoeOut*Coe*CoeTail? 的形式，也就是说，它可以由以下部分组成：
CoeHead 和 CoeOut 实例从推断类型朝预期类型方向成链。
换言之，会使用为该项得到的类型中的信息来解析实例链。
Coe 和 CoeTail 实例从预期类型朝推断类型方向成链，因此会使用预期类型中的信息来解析实例链。
如果这些链在中间相遇，就找到了一个强制转换。
这体现在它们的类型签名中：CoeHead 和 CoeOut 将半输出参数用于强制转换的目标，而 Coe 和 CoeTail 将半输出参数用于强制转换的源。
当实例为半输出参数提供值时，该值会在实例合成期间使用。
但是，如果没有提供值，则合成算法可以为其赋值。
因此，选择实例时，应为每个半输出参数指派一个类型。
这意味着，当强制转换输出中出现的变量是输入中变量的子集时，应使用 CoeOut；当输入中的变量是输出中变量的子集时，则应使用 Coe。
CoeOut 与 Coe 实例
Truthy 值由一个值和一个指示该值应视为真还是假的标志配对组成。
Decision 可以是 yes、no 或 maybe，其中最后一种还包含需要考虑的其他数据。
structure Truthy (α : Type) where
val : α
isTrue : Bool
inductive Decision (α : Type) where
| yes
| maybe (val : α)
| no
“Truthy” 值可以通过忽略其中包含的值转换为 Bool。
Bool 可以通过排除 maybe 情况转换为 Decision。
@[coe]
def Truthy.toBool : Truthy α → Bool :=
Truthy.isTrue
@[coe]
def Decision.ofBool : Bool → Decision α
| true => .yes
| false => .no
Truthy.toBool 必须是 CoeOut 实例，因为强制转换的目标比源包含更少的未知类型变量；而 Decision.ofBool 必须是 Coe 实例，因为强制转换的源比目标包含更少的变量：
instance : CoeOut (Truthy α) Bool := ⟨Truthy.isTrue⟩
instance : Coe Bool (Decision α) := ⟨Decision.ofBool⟩
有了这些实例，强制转换就可以成链：
#eval ({ val := 1, isTrue := true : Truthy Nat } : Decision String)
尝试使用错误的类会导致错误：
instance : Coe (Truthy α) Bool := ⟨Truthy.isTrue⟩
类型类
类型类
类型类
CoeTail α β 用于只能出现在强制转换序列末尾的转换。也就是说，α 还可以通过
Coe σ α 和 CoeHead τ σ 实例进一步转换，但 β 只能是表达式的预期类型。
实例构造子
CoeTail.mk.{u, v}
方法
coe : α → β
将类型为 α 的值强制转换为类型 β。可通过记法 ↑x 或双重类型标注 ((x : α) : β) 使用。
存在适当的实例链或单个适用的 CoeDep 实例时，可以合成 CoeT 的实例。从 Nat 强制转换到另一类型时，NatCast 实例也足够。
如果二者都存在，则优先使用 CoeDep 实例。
类型类
依赖强制转换不能成链。
作为强制转换链的替代方案，可以使用 CoeDep α e β 实例将类型为 α 的项 e 强制转换为 β。
依赖强制转换适用于只有部分值可以强制转换的情况；这一机制用于仅将可判定命题强制转换为 Bool。
当值本身出现在强制转换的目标类型中时，它们也很有用。
类型类
依赖强制转换
非空列表类型可以定义为一个列表与其非空证明组成的二元组。 通过应用投影，可以将此类型强制转换为普通列表：
structure NonEmptyList (α : Type u) : Type u where
contents : List α
non_empty : contents ≠ []
instance : Coe (NonEmptyList α) (List α) where
coe xs := xs.contents
该强制转换如预期般工作：
def oneTwoThree : NonEmptyList Nat := ⟨[1, 2, 3], ⊢ [1, 2, 3] ≠ [] All goals completed! 🐙⟩
#eval (oneTwoThree : List Nat) ++ [4]
然而，任意列表不能强制转换为非空列表，因为任意选取的某些列表确实可能为空：
instance : Coe (List α) (NonEmptyList α) where
coe xs := ⟨xs, _⟩
依赖强制转换可以把强制转换的定义域限制为非空列表：
instance : CoeDep (List α) (x :: xs) (NonEmptyList α) where
coe := ⟨x :: xs, α:Type ?u.7x:αxs:List α⊢ x :: xs ≠ [] All goals completed! 🐙⟩
#eval ([1, 2, 3] : NonEmptyList Nat)
插入依赖强制转换要求被转换的项在语法上与实例头中的项匹配。
已知非空、但在语法上不是 (· :: ·) 实例的列表，无法使用此实例进行强制转换。
#check
fun (xs : List Nat) =>
let ys : List Nat := xs ++ [4]
(ys : NonEmptyList Nat)
强制转换插入失败时，会报告原始类型错误：
与使用嵌套的类型标注不同，用于放置强制转换的 coeNotation : term↑ 语法不要求显式写出所涉及的类型。
控制强制转换插入
实例合成与强制转换插入会相互作用。 合成实例可能会使类型信息变为已知，随后触发强制转换插入。 强制转换的具体放置位置可能会影响结果。
在 sub 的这个定义中，会根据函数的返回类型合成 Sub Int 实例。
此实例要求两个参数也为 Int，但它们是 Nat。
减法运算符的每个实参外都会插入强制转换。
这可以从 Lean.Parser.Command.print : command#print 的输出中看出。
def sub (n k : Nat) : Int := n - k
#print sub
将强制转换运算符放在减法外部，会使精译器先尝试推断减法的类型，再插入强制转换。
因为实参都是 Nat，所以会选择 Sub Nat 实例，从而使差值成为 Nat。
然后再将该差值强制转换为 Int。
def sub' (n k : Nat) : Int := ↑ (n - k)
#print sub'
这两个函数并不等价，因为自然数减法会在零处截断：
#eval sub 4 8
#eval sub' 4 8
11.2.1. 实现强制转换
适当的 CoeHead、CoeOut、Coe 或 CoeTail 实例足以使所需的强制转换得以插入。
不过，强制转换的实现应使用 coe 属性注册为强制转换。
这会使 Lean 使用 coeNotation : term↑ 运算符显示强制转换的使用。
这也会使 norm_cast 策略将该强制转换视为数值转换，而不是普通函数。
属性强制转换声明
attr ::= ...
|
在函数上标记 @[coe] 属性（该函数通常也应出现在形如
instance : Coe A B := ⟨myFn⟩ 的声明中），可以让反精译器在打印表达式时把该函数的应用
显示为 ↑。
实现强制转换
inductive Weekday where
| mo | tu | we | th | fr | sa | su
作为一个七元素类型，它与 Fin 7 包含相同的信息。
二者之间存在双射：
def Weekday.toFin : Weekday → Fin 7
| mo => 0
| tu => 1
| we => 2
| th => 3
| fr => 4
| sa => 5
| su => 6
def Weekday.fromFin : Fin 7 → Weekday
| 0 => mo
| 1 => tu
| 2 => we
| 3 => th
| 4 => fr
| 5 => sa
| 6 => su
每种类型都可以强制转换为另一种：
instance : Coe Weekday (Fin 7) where
coe := Weekday.toFin
instance : Coe (Fin 7) Weekday where
coe := Weekday.fromFin
虽然这样可以工作，但 Lean 输出中出现的强制转换实例并未按 Lean 用户所期望的方式使用强制转换运算符呈现。
相反，其中显式使用了名称 Weekday.fromFin：
def wednesday : Weekday := (2 : Fin 7)
#print wednesday
为强制转换的定义添加 coe 属性，会使其使用强制转换运算符显示：
attribute [coe] Weekday.fromFin
attribute [coe] Weekday.toFin
def friday : Weekday := (5 : Fin 7)
#print friday
11.2.2. 自然数与整数的强制转换
类型类 NatCast 和 IntCast 是 Coe 的特殊情况，用于定义从 Nat 或 Int 到某种在一定意义上具有典范性的其他类型的强制转换。
它们的存在是为了更好地集成大型数学库，例如 Mathlib；这类库大量使用强制转换，将自然数或整数映射到其他结构（通常是环）。
理想情况下，将自然数或整数强制转换到这些结构所得的形式应为simp 规范形，因为这是一种方便的表示方式。
当强制转换的应用预期成为某类型的simp 规范形时，重要的是实践中所有这类强制转换都应定义相等。
否则，simp 规范形就必须选择唯一一条成链的强制转换路径，但引理却可能不慎使用另一条路径来陈述。
由于 simp 的内部索引基于项的底层结构，而不是项在表层语法中的呈现方式，这些差异会使引理无法在预期位置应用。
另一方面，NatCast 和 IntCast 实例应定义成始终定义相等，从而避免这个问题。
Lean 标准库对实例的安排使得插入强制转换时，会优先选择 NatCast 或 IntCast 实例，而不是强制转换实例链。
它们也可以用作 CoeOut 实例，从而在需要时平稳回退到强制转换链。
类型类
定义
类型类