what does the colon greater than sign mean in coq

Question

For example

Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}.

what does the ":>" mean? I hope this isn't a duplicate, but a symbol is hard to search for.

Answer 1

In this particular case it inserts a Coercion from the posreal record to its field pos. This means you can use a posreal for an R in most cases.

Try:

Definition idR (x : R) := x.
Variable (r : posreal).
Compute (idR r).

See https://coq.inria.fr/refman/Reference-Manual021.html#Coercions-and-records