coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to access the elements of a record in coq

From: "Namio Namelander" <verifying AT ndtvmail.com>
To: <coq-club AT inria.fr>
Subject: [Coq-Club] How to access the elements of a record in coq
Date: Thu, 13 Nov 2014 15:43:15 -0800

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.

[Coq-Club] How to access the elements of a record in coq, Namio Namelander, 11/14/2014
- Re: [Coq-Club] How to access the elements of a record in coq, Eddy Westbrook, 11/14/2014
  - Re: [Coq-Club] How to access the elements of a record in coq, Cedric Auger, 11/14/2014