11.5. 实施细节🔗

只有普通的强制插入才使用链接。将强制转换插入 sort 或 function 使用普通实例合成。同样，依赖强制转换也不是链接的。

11.5.1. 展开强制🔗

强制插入机制展开了强制的应用，这使得它们能够控制结果项的特定形状。这对于确保可读的证明目标和控制编译代码中强制术语的评估都很重要。展开强制转换由 coe_decl 属性控制，该属性应用于每种强制转换方法（例如 Coe.coe）。该属性应被视为强制机制内部的一部分，而不是公共强制 API 的一部分。

11.5.2. 强制链接🔗

强制链接是通过辅助类型类的集合来实现的。用户不应直接编写这些类的实例，但在诊断未按预期插入强制转换的原因时，了解其结构可能很有用。管理链中实例排序的特定规则（即，它应该匹配 CoeHead?CoeOut*Coe*CoeTail?）由以下类型类：

CoeTC 是 Coe 实例的传递闭包。
CoeOTC 是链的中间，由 CoeOut 实例的传递闭包和后跟的 CoeTC 组成。
CoeHTC 是链的起点，最多由一个 CoeHead 实例组成，后跟 CoeOTC。
CoeHTCT 是整个链，由 CoeHTC 和最多一个 CoeTail 实例组成。或者，它可能是 NatCast 实例。
CoeT 代表整个链：它可以是 CoeHTCT 链，也可以是单个 CoeDep 实例。

Auxiliary Classes for Coercions

type class

CoeHTCT.{u, v} (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)
CoeHTCT.{u, v} (α : Sort u) (β : Sort v) :
  Sort (max (max 1 u) v)

Auxiliary class implementing CoeHead* Coe* CoeTail?. Users should generally not implement this directly.

Instance Constructor

CoeHTCT.mk.{u, v}

Methods

coe : α → β

Coerces a value of type α to type β. Accessible by the notation ↑x, or by double type ascription ((x : α) : β).

type class

CoeHTC.{u, v} (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)
CoeHTC.{u, v} (α : Sort u) (β : Sort v) :
  Sort (max (max 1 u) v)

Auxiliary class implementing CoeHead CoeOut* Coe*. Users should generally not implement this directly.

Instance Constructor

CoeHTC.mk.{u, v}

Methods

coe : α → β

Coerces a value of type α to type β. Accessible by the notation ↑x, or by double type ascription ((x : α) : β).

type class

CoeOTC.{u, v} (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)
CoeOTC.{u, v} (α : Sort u) (β : Sort v) :
  Sort (max (max 1 u) v)

Auxiliary class implementing CoeOut* Coe*. Users should generally not implement this directly.

Instance Constructor

CoeOTC.mk.{u, v}

Methods

coe : α → β

Coerces a value of type α to type β. Accessible by the notation ↑x, or by double type ascription ((x : α) : β).

type class

CoeTC.{u, v} (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)
CoeTC.{u, v} (α : Sort u) (β : Sort v) :
  Sort (max (max 1 u) v)

Auxiliary class implementing Coe*. Users should generally not implement this directly.

Instance Constructor

CoeTC.mk.{u, v}

Methods

coe : α → β

Coerces a value of type α to type β. Accessible by the notation ↑x, or by double type ascription ((x : α) : β).