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:33:21 -0500
Authentication-results: mail3-smtp-sop.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:LpfaSRRMhrctHGbWm0qCAR+Jqtpsv+yvbD5Q0YIujvd0So/mwa64YB2N2/xhgRfzUJnB7Loc0qyN4/6mCTFLuMvJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipduDPk4R2XKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtGbdfFXEtN30/zMztrxjKCwWVsCgySGITxzZVGRfM9h2ye5zdtS33su41jAWHJ9L/V7xyfD+O6KFmTBvAiicaPiY9tmzbl5oj3+pgvBu9qkknkMbva4aPOa8mcw==

On 01/12/2016 11:26 AM, John Wiegley wrote:
>>>>>> Durward McDonell
>>>>>> <Durward.McDonell AT jhuapl.edu>
>>>>>> writes:
>
>> But now I cannot access, e.g., ZMCT.ops.compare (or ZMCT.ops.(compare), or
>> (compare ZMCT.ops)). How do I do something interesting with ZMCT?
>
> Did you mean ZMCT.Ops.compare?
>

I don't think so. ZMCT.Ops isn't a thing. Module ZModuloCyclicType
defines Instance ops.

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