这可能是非常微不足道的，但我找不到任何关于 ':>' 符号在 Coq 中含义的信息。
有什么区别：
U：类型
和
W :> 类型
？
这取决于符号出现的位置。例如，如果它位于记录声明内，它会指示 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投影。如果我们用过:代替:>, only bar'将被 Coq 接受，并且bar会引发类型错误。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
