The Coq mailing list

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

Hello.

I am trying to use the ZModulo library, and having some difficulty
accessing ops and specs. Here are some relevant bits:

In CyclicAxioms.v we have

Module ZnZ.
  Class Ops (t:Type) := MkOps {
    ...
    compare : t -> t -> comparison; (* e.g. *)
    ...
  }.
  (* And something similar for Specs. *)
End ZnZ.

In ZModulo.v we have

Section ZModulo.
  Variable digits : positive.
  Hypothesis digits_ne_1 : digits <> 1%positive.
  ...
  (* Definitions for everything in ZnZ.Ops and ZnZ.Specs. *)
  ...
  Instance zmod_ops : ZnZ.Ops Z := ZnZ.MkOps (* Here is a list of
previous definitions. *).
  Instance zmod_specs : ZnZ.Specs zmod_ops := ZnZ.MkSpecs (* Here is a
list of previous definitions. *).
End ZModulo.

Module Type PositiveNotOne.
  Parameter p : positive.
  Axiom not_one : p <> 1%positive.
End PositiveNotOne.

Module ZModuloCyclicType (P:PositiveNotOne) <: CyclicType.
 Definition t := Z.
 Instance ops : ZnZ.Ops t := zmod_ops P.p.
 Instance specs : ZnZ.Specs ops := zmod_specs P.not_one.
End ZModuloCyclicType.

In foo.v, I have put (omitting scopes and imports)

Module PNO : PositiveNotOne.
  Definition p := 3%positive.  (* I.e., we want 3-bit numbers with
cyclic addition. *)
  Lemma not_one : p <> 1%positive.
  Proof.
    unfold p.
    discriminate.
  Qed.
End PNO.

Module ZMCT := ZModuloCyclicType PNO.

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?

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

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