The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

The fields of a record become projection functions. So, in your definition, universe has type ToyModel -> Set, i.e., when applied to a ToyModel, universe projects out and returns the universe component of it. Similarly with the other fields you have defined.

From there, you should hopefully be able to write your definition. :)

-E

On Nov 13, 2014, at 3:43 PM, Namio Namelander <verifying AT ndtvmail.com> wrote:

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 this in coq? The problem is that I don't know
how to access the elements inside a record.