CODEWITHSUNDEEP
coq
verifying
verifying

Reputation: 39

How to access the elements of a record in coq

Suppose I have a record

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

I would like to define a notion of compatibility for elements of type 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.

How can I write that in coq? The problem is that I don't know how to access the elements inside a record.

Upvotes: 0

Views: 1470

Answers (1)

Ptival
Ptival

Reputation: 9437

The fields of the record become accessor functions for it, so it should just be a matter of:

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

Or:

t.(universe)
t.(color) u

You might have to:

Set Printing Projections.

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

Upvotes: 2

Related Questions