什麼結腸大於號在COQ

2016-12-16 44 views 4 likes

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

什麼是「：>」是什麼意思？我希望這不是重複的，但一個符號很難搜索。

2016-12-16 davik

有其他含義的'：>'符號。除非你對所有的含義都感興趣，否則最好讓問題的標題更加精確。 –

回答

在這種特殊情況下，它會將來自posreal記錄的強制轉換爲其字段pos。這意味着在大多數情況下，您可以使用posreal作爲R。

嘗試：

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

2016-12-16 20:09:32 ejgallego

啊，我懷疑這是一種繼承，謝謝 – davik