What a push larger than a sign means in coq

Question

for instance

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

What does ":>" mean? I hope this is not a duplicate, but it is difficult to find.

Answer 1

In this particular case, he inserts the coercion from the record posrealinto his field pos. This means that you can use posrealfor Rmost 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