什麼結腸大於​​號在COQ

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