The Coq mailing list

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

Thank you for your help. Yes, ZnZ.compare was the right answer,
which makes sense to me now.

On 01/12/2016 11:49 AM, Sosuke MORIGUCHI wrote:
> 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.)
>>
> 


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

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