The Coq mailing list

[Durward McDonell <Durward.McDonell AT jhuapl.edu>]

Thank you. I actually figured this out, mostly through random
thrashing, but it makes sense now.

On 01/13/2016 01:29 AM, Arnaud Spiwack wrote:
> 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
>  
> <mailto: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
>  
> <mailto:durward.mcdonell AT jhuapl.edu>
>     240-228-2690 <tel:240-228-2690> (DC)
>     443-778-2690 <tel:443-778-2690> (Balt.)
> 
> 


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

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