The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

For information, records are just inductives.

Thus your type is in fact:

Inductive ToyModel:=
X : forall
    (universe:Set)
    (aNiceProperty:universe->Prop)
    (color:universe->nat),
    ToyModel.

Where "X" is automatically generated, along with projections as said by Eddy.
I think you can find out this generated name with "Print ToyModel."

To extract "universe" from "tm" you can do the following:
- match tm with X (*to be replaced by its real name*) uni _ _ => uni end
- let (uni, _, _) := tm in uni (* syntactic shorthand for single constructor types *)
- universe tm
- tm.(universe) (* access field for records [in fact a notation for "universe tm"] *)

2014-11-14 1:06 GMT+01:00 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.

--

.../Sedrikov\...