如何訪問記錄的元素COQ

Question

假設我有一個記錄

Record ToyModel:={ 
universe:Set; 
aNiceProperty:universe->Prop; 
color:universe->nat 
}. 

我想定義兼容性的概念，類型ToyModel的 元素。

Definition Compatible(T1 T2: ToyModel):= 
if there is an element of T1.universe with color a then there 
exists an element of T2.universe with color a. 

我該怎麼寫coq？問題是我不知道 如何訪問記錄中的元素。

Answer 1

爲它記錄成爲訪問函數的領域，所以它應該只是一個問題的：

universe t (* where t : ToyModel *) 
color t u (* where t : ToyModel, u : universe *) 

或者：

t.(universe) 
t.(color) u 

您可能需要：

Set Printing Projections. 

比較https://coq.inria.fr/distrib/current/refman/Reference-Manual004.html#toc15