结肠大于标志的结果是什么意思

Question

例如

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

":>"是什么意思？我希望这不是重复,但很难找到符号.

Answer 1

在这种特殊情况下,它会将posreal记录中的强制插入到其字段中pos.这意味着你可以使用posreal一个R在大多数情况下.

尝试:

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

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