что означает это обозначение `:>` в Coq? - PullRequest
Новая
       12

что означает это обозначение `:>` в Coq?

0 голосов
/ 25 апреля 2019

Я видел, что нотация :> используется внутри определения типа записи. Не уверен, что это стандартная запись или она определена где-то в файле, который я смотрю.

1 Ответ

1 голос
/ 25 апреля 2019

Объявляет приведение из записи в это поле.

Например, если у вас есть запись: 

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

...