Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Accessing Class members

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Accessing Class members


Chronological Thread 
  • From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Accessing Class members
  • Date: Wed, 13 Jan 2016 07:29:16 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=arnaud.spiwack AT gmail.com; spf=Pass smtp.mailfrom=arnaud.spiwack AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f41.google.com
  • Ironport-phdr: 9a23:AMKE2hDQj7YPco6OLY+tUyQJP3N1i/DPJgcQr6AfoPdwSP7zp8bcNUDSrc9gkEXOFd2CrakU1ayG7euxBCQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTpkbDssMyOKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ6jiR6WZgyWrlAYT29exhFPGk3O6Azwdpb3qCrz8ORnjnq0J8rzGJkuXz2/4+9QUB73gSwEf2ow63nWlcV7j4pfoQLnvxt70pLZa4GTNeNjc+XTZ4VJFiJ6Qs9NWnkZUcuHZIwVAr9EZL4Aog==
ZnZ.compare ZMCT.ops

should do the trick: class projections are in the module that defined the class.

On 12 January 2016 at 17:58, Durward McDonell <Durward.McDonell AT jhuapl.edu> wrote:

I should have posted a working foo.v. Here it is:

Require Import ZModulo.
Require Import ZArith.
Require Import DoubleType.
Require Import CyclicAxioms.

Set Implicit Arguments.

Open Scope positive_scope.

Module PNO : PositiveNotOne.
  Definition p := 3.
  Lemma not_one : p <> 1%positive.
  Proof.
    unfold p.
    discriminate.
  Qed.
End PNO.

Close Scope positive_scope.
Open Scope Z_scope.

Module ZMCT <: CyclicType := ZModuloCyclicType PNO.

At this point, ZMCT.t, ZMCT.ops, and ZMCT.specs will all happily let
you Print their types, but you cannot access any of the members of
ZMCT.ops or ZMCT.specs, as far as I can tell.

--
Durward McDonell
durward.mcdonell AT jhuapl.edu
240-228-2690 (DC)
443-778-2690 (Balt.)



Archive powered by MHonArc 2.6.18.

Top of Page