这个符号`：>`在Coq中意味着什么？

Question

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

Answer 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