Coq :>符号

Question

这可能非常琐碎，但我在Coq中找不到关于':>‘符号的任何信息。U:类型和W :>类型有什么区别？

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理解每个T : foo都可以出现在它期望类型的位置，方法是将它封装在sort投影周围。如果我们使用:而不是:>，Coq将只接受bar'，而bar将引发类型错误。