diff options
Diffstat (limited to 'theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v')
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v index 28d40094..88cbb484 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v @@ -8,12 +8,12 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: DoubleType.v 10964 2008-05-22 11:08:13Z letouzey $ i*) +(*i $Id$ i*) Set Implicit Arguments. Require Import ZArith. -Open Local Scope Z_scope. +Local Open Scope Z_scope. Definition base digits := Zpower 2 (Zpos digits). @@ -37,10 +37,10 @@ Section Zn2Z. Variable znz : Type. - (** From a type [znz] representing a cyclic structure Z/nZ, + (** From a type [znz] representing a cyclic structure Z/nZ, we produce a representation of Z/2nZ by pairs of elements of [znz] - (plus a special case for zero). High half of the new number comes - first. + (plus a special case for zero). High half of the new number comes + first. *) Inductive zn2z := @@ -57,10 +57,10 @@ End Zn2Z. Implicit Arguments W0 [znz]. -(** From a cyclic representation [w], we iterate the [zn2z] construct - [n] times, gaining the type of binary trees of depth at most [n], - whose leafs are either W0 (if depth < n) or elements of w - (if depth = n). +(** From a cyclic representation [w], we iterate the [zn2z] construct + [n] times, gaining the type of binary trees of depth at most [n], + whose leafs are either W0 (if depth < n) or elements of w + (if depth = n). *) Fixpoint word (w:Type) (n:nat) : Type := |