这个符号 `:>` 在 Coq 中是啥意思？

Posted 2023-05-08

【中文标题】这个符号 `:>` 在 Coq 中是啥意思？

【英文标题】：what does this notation `:>` mean in Coq?这个符号 `:>` 在 Coq 中是什么意思？

【发布时间】：2019-09-14 06:57:16

【问题描述】：

我看到在记录数据类型定义中使用了:> 表示法。 不确定这是否是标准符号，或者它是否在我正在查看的文件中的某处定义。

【参考方案1】：

它声明了从记录到该字段的强制。

例如，如果您有记录：

Record foo :=
   f1 :> bar
  ; f2 : baz
  .

如果你有x : foo，那么你可以把它放在需要bar的地方，f1的应用程序会自动插入。

x : bar
(* will desugar to (f1 x : bar), though it will still be hidden by Coq's prettyprinter. *)

更多详情请看手册：https://coq.inria.fr/distrib/current/refman/addendum/implicit-coercions.html#classes-as-records