Coq :> 符号

Question

这可能是非常微不足道的，但我找不到任何关于 ':>' 符号在 Coq 中含义的信息。U : Type 和 W :> Type 之间有什么区别？

Answer 1

这取决于符号出现的位置。例如，如果它位于记录声明内，它会指示 Coq 添加相应的记录投影作为强制。

具体来说，假设我们有以下带有操作的类型定义：

Record foo := Foo {
  sort :> Type;
  op   : sort -> sort -> sort
}.

我们现在可以编写以下函数，该函数应用该结构的操作两次：

Definition bar (T : foo) (x y z : T) : T :=
  op foo x (op foo y z).

通过使用该:>符号，我们指示 Coq 读取 的定义，bar如下所示：

Definition bar' (T : foo) (x y z : sort T) : sort T :=
  op foo x (op foo y z).

也就是说，Coq 知道 everyT : foo可以通过将其包裹在投影周围而出现在它期望类型的位置sort。如果我们使用:而不是:>，则只会bar'被 Coq 接受，并且bar会引发类型错误。