coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Accessing Class members

From: Durward McDonell <Durward.McDonell AT jhuapl.edu>
To: <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Accessing Class members
Date: Tue, 12 Jan 2016 11:58:10 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Durward.McDonell AT jhuapl.edu; spf=Pass smtp.mailfrom=Durward.McDonell AT jhuapl.edu; spf=Pass smtp.helo=postmaster AT pilot.jhuapl.edu
Ironport-phdr: 9a23:LAMbwR25E8RPDKXTsmDT+DRfVm0co7zxezQtwd8ZsegSI/ad9pjvdHbS+e9qxAeQG96LtbQU1qGP4+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6MyZTqnLnis7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JsUWqLjOq88ULZwDTI8Mmlz6te95jfZSg7aymYGTWwMnlJtCCTC6hz+Wt+lnjbgqeNn1G+/NuHxS70wXRyg77piUBuuhSsaYW1quFrLg9B92foI6CmqoAZyltbZ

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.)

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

[Coq-Club] Accessing Class members, Durward McDonell, 01/12/2016
- Re: [Coq-Club] Accessing Class members, John Wiegley, 01/12/2016
  - Re: [Coq-Club] Accessing Class members, Durward McDonell, 01/12/2016
- Re: [Coq-Club] Accessing Class members, Sosuke MORIGUCHI, 01/12/2016
  - Re: [Coq-Club] Accessing Class members, Durward McDonell, 01/13/2016
- Re: [Coq-Club] Accessing Class members, Durward McDonell, 01/12/2016
  - Re: [Coq-Club] Accessing Class members, Arnaud Spiwack, 01/13/2016
    - Re: [Coq-Club] Accessing Class members, Durward McDonell, 01/13/2016