相关疑难解决方法(0)

例如

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

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