The Coq mailing list

[Sosuke MORIGUCHI <chiguri.s AT gmail.com>]

It looks you cannot see the projection function "compare" (for Ops)
from your place.
How about to use "Import ZnZ." before you access or "ZnZ.compare"
instead of "compare"?

2016-01-13 0:01 GMT+09:00 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.)
>