The Coq :> symbol

问题:

This is probably super trivial, but I can't find any information about what the ':>' symbol means in Coq. What is the difference between: U : Type and W :> Type ?

回答1:

It depends on where the symbol occurs. If it is inside a record declaration, for instance, it instructs Coq to add the corresponding record projection as a coercion.

Concretely, suppose that we have the following definition of a type with an operation:

Record foo := Foo {
  sort :> Type;
  op   : sort -> sort -> sort
}.

We can now write the following function, which applies the operation of the structure twice:

Definition bar (T : foo) (x y z : T) : T :=
  op foo x (op foo y z).

By using the :> symbol, we have instructed Coq to read the definition of bar as the following one:

Definition bar' (T : foo) (x y z : sort T) : sort T :=
  op foo x (op foo y z).

That is, Coq understands that every T : foo can appear in a position where it expects a type, by wrapping it around the sort projection. Had we used : instead of :>, only bar' would be accepted by Coq, and bar would raise a type error.