冒号中大于冒号的含义是什么 [英] what does the colon greater than sign mean in coq

问题描述

例如

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.

推荐答案

情况下，它会从 posreal 记录向其字段 pos 插入一个强制。这意味着在大多数情况下，您可以将 posreal 用于 R 。

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.

尝试：

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

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

这篇关于冒号中大于冒号的含义是什么的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！