Coq：>符号 [英] The Coq :> symbol

问题描述

这可能是微不足道的，但我无法找到有关Coq中：>符号含义的任何信息。
之间有什么区别：
U：键入
和
W：>键入
吗？

This is probably super trivial, but I can't find any information about what the ':>' symbol means in Coq. What is the difference between: U : Type and W :> Type ?

推荐答案

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

It depends on where the symbol occurs. If it is inside a record declaration, for instance, it instructs Coq to add the corresponding record projection as a coercion.

具体地，假设我们对a具有以下定义

Concretely, suppose that we have the following definition of a type with an operation:

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

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

We can now write the following function, which applies the operation of the structure twice:

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

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

By using the :> symbol, we have instructed Coq to read the definition of bar as the following one:

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

也就是说，Coq知道每个 T：foo 包裹在 sort 投影周围，可以将其显示在期望类型的位置。如果我们使用：代替：> ，只有 bar'将被Coq接受，并且 bar 会引发类型错误。

That is, Coq understands that every T : foo can appear in a position where it expects a type, by wrapping it around the sort projection. Had we used : instead of :>, only bar' would be accepted by Coq, and bar would raise a type error.

这篇关于Coq：>符号的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！