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

【问题标题】：what does this notation `:>` mean in Coq?这个符号 `:>` 在 Coq 中是什么意思？
【发布时间】：2019-09-14 06:57:16
【问题描述】：

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

【问题讨论】：

标签： coq

【解决方案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. *)

【讨论】：