diff options
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CyclicAxioms.v (renamed from theories/Numbers/Cyclic/Abstract/Z_nZ.v) | 7 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 11 |
2 files changed, 13 insertions, 5 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/Z_nZ.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index 6d19e6613..ed14cc799 100644 --- a/theories/Numbers/Cyclic/Abstract/Z_nZ.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -12,6 +12,9 @@ (** * Signature and specification of a bounded integer structure *) +(** This file specifies how to represent [Z/nZ] when [n=2^d], + [d] being the number of digits of these bounded integers. *) + Set Implicit Arguments. Require Import ZArith. @@ -30,7 +33,7 @@ Section Z_nZ_Op. Record znz_op : Set := mk_znz_op { (* Conversion functions with Z *) - znz_digits : positive; + znz_digits : positive; znz_zdigits: znz; znz_to_Z : znz -> Z; znz_of_pos : positive -> N * znz; @@ -40,7 +43,7 @@ Section Z_nZ_Op. (* Basic constructors *) znz_0 : znz; znz_1 : znz; - znz_Bm1 : znz; + znz_Bm1 : znz; (* [2^digits-1], which is equivalent to [-1] *) znz_WW : znz -> znz -> zn2z znz; znz_W0 : znz -> zn2z znz; znz_0W : znz -> zn2z znz; diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index df3af4b63..2d23a12dd 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -13,10 +13,15 @@ Require Export NZAxioms. Require Import BigNumPrelude. Require Import DoubleType. -Require Import Z_nZ. +Require Import CyclicAxioms. -(** * A Z/nZ representation (module type [CyclicType]) implements - [NZAxiomsSig], e.g. the common properties between N and Z. *) +(** * From [CyclicType] to [NZAxiomsSig] *) + +(** A [Z/nZ] representation given by a module type [CyclicType] + implements [NZAxiomsSig], e.g. the common properties between + N and Z with no ordering. Notice that the [n] in [Z/nZ] is + a power of 2. +*) Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZAxiomsSig. |