当 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
由于强制链接，还存在从 Even 到 Int 的强制，通过将 Coe Even Nat 实例与从 Nat 到 Int 的现有强制链接链接起来形成：
#eval (four : Int) - 5
当需要被强制的特定术语时，需要 Dependent coercions，以便确定是否或如何强制该术语：例如，只有可判定命题可以强制为 Bool，因此相关命题必须作为实例类型的一部分出现，以便它可以需要 Decidable 实例。
只要推断类型的所有值都可以强制转换为目标类型，就会使用非依赖强制转换。
非依赖强制转换可以是链接的：如果存在从 α 到 β 以及从 β 到 γ 的强制转换，则还存在从 α 到 γ 的强制转换。
该链的格式应为 CoeHead?CoeOut*Coe*CoeTail?，也就是说它可能包含以下内容：
CoeHead 和 CoeOut 实例从推断类型链接到预期类型。
换句话说，为该术语找到的类型中的信息用于解析实例链。
Coe 和 CoeTail 实例从预期类型链接到推断类型，因此预期类型中的信息用于解析实例链。
如果这些链在中间相遇，则发现了强制。
这反映在它们的类型签名中：CoeHead 和 CoeOut 使用 半输出参数 作为强制转换的目标，而 Coe 和 CoeTail 使用 半输出参数 作为强制转换的源。
当实例为 半输出参数 提供值时，该值将在实例综合期间使用。
然而，如果没有提供值，则合成算法可以分配一个值。
因此，在选择实例时，应为每个半输出参数分配一个类型。
这意味着当强制输出中出现的变量是其输入中的变量的子集时，应使用 CoeOut；当输入中的变量是输出中的变量的子集时，应使用 Coe。
CoeOut vs Coe instances
Truthy 值是与是否应将其视为 true 或 false 的指示配对的值。
Decision 是 yes、no 或 maybe，后者包含供考虑的更多数据。
structure Truthy (α : Type) where
val : α
isTrue : Bool
inductive Decision (α : Type) where
| yes
| maybe (val : α)
| no
通过忘记包含的值，“Truthy” 值可以转换为 Bool。
通过打折 maybe 外壳，Bool 可以转换为 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⟩
CoeHead α β is for coercions that are applied from left-to-right at most once
at beginning of the coercion chain.
CoeHead.mk.{u, v}
coe : α → β
Coerces a value of type α to type β. Accessible by the notation ↑x,
or by double type ascription ((x : α) : β).
CoeTail α β is for coercions that can only appear at the end of a
sequence of coercions. That is, α can be further coerced via Coe σ α and
CoeHead τ σ instances but β will only be the expected type of the expression.
CoeTail.mk.{u, v}
coe : α → β
Coerces a value of type α to type β. Accessible by the notation ↑x,
or by double type ascription ((x : α) : β).
当存在适当的实例链时，或者当存在单个适用的 CoeDep 实例时，可以合成 CoeT 的实例。从 Nat 强制到另一种类型时，NatCast 实例也足够了。
如果两者都存在，则 CoeDep 实例优先。
CoeT is the core typeclass which is invoked by Lean to resolve a type error.
It can also be triggered explicitly with the notation ↑x or by double type
ascription ((x : α) : β).
A CoeT chain has the grammar CoeHead? CoeOut* Coe* CoeTail? | CoeDep.
CoeT.mk.{u, v}
coe : β
The resulting value of type β. The input x : α is a parameter to
the type class, so the value of type β may possibly depend on additional
typeclasses on x.
依赖强制不能被链接。
作为强制链的替代方案，可以使用 CoeDep α e β 的实例将类型 α 的术语 e 强制为 β。
依赖强制转换在只能强制强制某些值的情况下很有用；该机制用于将可判定命题强制强制为 Bool。
当值本身出现在强制转换的目标类型中时，它们也很有用。
CoeDep α (x : α) β is a typeclass for dependent coercions, that is, the type β
can depend on x (or rather, the value of x is available to typeclass search
so an instance that relates β to x is allowed).
Dependent coercions do not participate in the transitive chaining process of regular coercions: they must exactly match the type mismatch on both sides.
CoeDep.mk.{u, v}
coe : β
The resulting value of type β. The input x : α is a parameter to
the type class, so the value of type β may possibly depend on additional
typeclasses on x.
非空列表的类型可以定义为一对列表和证明它不为空的证明。 可以通过应用投影将此类型强制为普通列表：
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)
强制插入失败时，报原始类型错误：
term ::= ...
| `↑x` represents a coercion, which converts `x` of type `α` to type `β`, using
typeclasses to resolve a suitable conversion function. You can often leave the
`↑` off entirely, since coercion is triggered implicitly whenever there is a
type error, but in ambiguous cases it can be useful to use `↑` to disambiguate
between e.g. `↑x + ↑y` and `↑(x + y)`.
可以使用前缀运算符 coeNotation : term`↑x` represents a coercion, which converts `x` of type `α` to type `β`, using
typeclasses to resolve a suitable conversion function. You can often leave the
`↑` off entirely, since coercion is triggered implicitly whenever there is a
type error, but in ambiguous cases it can be useful to use `↑` to disambiguate
between e.g. `↑x + ↑y` and `↑(x + y)`.
↑ 显式放置强制转换。
与使用嵌套 类型归属 不同，用于放置强制转换的 coeNotation : term`↑x` represents a coercion, which converts `x` of type `α` to type `β`, using
typeclasses to resolve a suitable conversion function. You can often leave the
`↑` off entirely, since coercion is triggered implicitly whenever there is a
type error, but in ambiguous cases it can be useful to use `↑` to disambiguate
between e.g. `↑x + ↑y` and `↑(x + y)`.
↑ 语法不需要显式编写所涉及的类型。
实例合成和强制插入是相互作用的。 合成实例可以使类型信息已知，随后触发强制插入。 强制的具体位置可能很重要。
在 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
适当的 CoeHead、CoeOut、Coe 或 CoeTail 实例足以导致插入所需的强制。
但是，强制的实现应使用 coe 属性注册为强制。
这会导致 Lean 显示 coeNotation : term`↑x` represents a coercion, which converts `x` of type `α` to type `β`, using
typeclasses to resolve a suitable conversion function. You can often leave the
`↑` off entirely, since coercion is triggered implicitly whenever there is a
type error, but in ambiguous cases it can be useful to use `↑` to disambiguate
between e.g. `↑x + ↑y` and `↑(x + y)`.
↑ 运算符的强制转换的使用情况。
它还导致 norm_cast策略将强制转换视为强制转换，而不是普通函数。
attr ::= ...
| The `@[coe]` attribute on a function (which should also appear in a
`instance : Coe A B := ⟨myFn⟩` declaration) allows the delaborator to show
applications of this function as `↑` when printing expressions.
The @[coe] attribute on a function (which should also appear in a
instance : Coe A B := ⟨myFn⟩ declaration) allows the delaborator to show
applications of this function as ↑ when printing expressions.
enum inducing 类型 Weekday 代表一周中的几天：
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
类型类 NatCast 和 IntCast 是 Coe 的特殊情况，用于定义从 Nat 或 Int 到某种某种意义上规范的其他类型的强制。
它们的存在是为了更好地与大型数学库集成，例如 Mathlib，这些数学库大量使用强制从自然数或整数映射到其他结构（通常是环）。
理想情况下，将自然数或整数强制转换为这些结构是 simp 范式，因为这是表示它们的便捷方法。
当强制转换应用程序预计为类型的 simp 范式 时，重要的是在实践中所有此类强制转换都是 定义等价。
否则，simp范式将需要选择单个链式强制转换路径，但引理可能会意外地使用不同的路径来陈述。
由于 simp 的内部索引基于术语的底层结构，而不是其在表面语法中的表示形式，因此这些差异将导致引理无法应用到预期的位置。
另一方面，NatCast 和 IntCast 实例应定义为始终 定义等价，从而避免出现该问题。
Lean 标准库的实例经过排列，使得在强制插入期间优先选择 NatCast 或 IntCast 实例而不是强制实例链。
它们还可以用作 CoeOut 实例，允许在需要时优雅地回退到强制链接。
The canonical homomorphism Nat → R. In most use cases, the target type will have a (semi)ring
structure, and this homomorphism should be a (semi)ring homomorphism.
NatCast and IntCast exist to allow different libraries with their own types that can be notated
as natural numbers to have consistent simp normal forms without needing to create coercion
simplification sets that are aware of all combinations. Libraries should make it easy to work with
NatCast where possible. For instance, in Mathlib there will be such a homomorphism (and thus a
NatCast R instance) whenever R is an additive monoid with a 1.
The prototypical example is Int.ofNat.
NatCast.mk.{u}
natCast : Nat → R
The canonical map Nat → R.
The canonical homomorphism Nat → R. In most use cases, the target type will have a (semi)ring
structure, and this homomorphism should be a (semi)ring homomorphism.
NatCast and IntCast exist to allow different libraries with their own types that can be notated
as natural numbers to have consistent simp normal forms without needing to create coercion
simplification sets that are aware of all combinations. Libraries should make it easy to work with
NatCast where possible. For instance, in Mathlib there will be such a homomorphism (and thus a
NatCast R instance) whenever R is an additive monoid with a 1.
The prototypical example is Int.ofNat.
The canonical homomorphism Int → R. In most use cases, the target type will have a ring structure,
and this homomorphism should be a ring homomorphism.
IntCast and NatCast exist to allow different libraries with their own types that can be notated
as natural numbers to have consistent simp normal forms without needing to create coercion
simplification sets that are aware of all combinations. Libraries should make it easy to work with
IntCast where possible. For instance, in Mathlib there will be such a homomorphism (and thus an
IntCast R instance) whenever R is an additive group with a 1.
IntCast.mk.{u}
intCast : Int → R
The canonical map Int → R.
The canonical homomorphism Int → R. In most use cases, the target type will have a ring structure,
and this homomorphism should be a ring homomorphism.
IntCast and NatCast exist to allow different libraries with their own types that can be notated
as natural numbers to have consistent simp normal forms without needing to create coercion
simplification sets that are aware of all combinations. Libraries should make it easy to work with
IntCast where possible. For instance, in Mathlib there will be such a homomorphism (and thus an
IntCast R instance) whenever R is an additive group with a 1.