11.5. 实现细节🔗

只有普通强制转换插入会使用强制转换链。插入强制转换为 Sort 或函数类型时，使用普通实例合成。同样，依赖强制转换不会链接。

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 实例。

强制转换的辅助类

类型类

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)

实现 CoeHead* Coe* CoeTail? 的辅助类。用户通常不应直接实现该类。

实例构造子

CoeHTCT.mk.{u, v}

方法

coe : α → β

将类型为 α 的值强制转换为类型 β。可通过记法 ↑x 或双重类型标注 ((x : α) : β) 使用。

类型类

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)

实现 CoeHead CoeOut* Coe* 的辅助类。用户通常不应直接实现该类。

实例构造子

CoeHTC.mk.{u, v}

方法

coe : α → β

将类型为 α 的值强制转换为类型 β。可通过记法 ↑x 或双重类型标注 ((x : α) : β) 使用。

类型类

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)

实现 CoeOut* Coe* 的辅助类。用户通常不应直接实现该类。

实例构造子

CoeOTC.mk.{u, v}

方法

coe : α → β

将类型为 α 的值强制转换为类型 β。可通过记法 ↑x 或双重类型标注 ((x : α) : β) 使用。

类型类

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)

实现 Coe* 的辅助类。用户通常不应直接实现该类。

实例构造子

CoeTC.mk.{u, v}

方法

coe : α → β

将类型为 α 的值强制转换为类型 β。可通过记法 ↑x 或双重类型标注 ((x : α) : β) 使用。