diff options
Diffstat (limited to 'theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v')
-rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v index 95f3c88e6..dfc8b4e32 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v @@ -25,6 +25,12 @@ Section Carry. | C0 : A -> carry | C1 : A -> carry. + Definition interp_carry (sign:Z)(B:Z)(interp:A -> Z) c := + match c with + | C0 x => interp x + | C1 x => sign*B + interp x + end. + End Carry. Section Zn2Z. @@ -47,12 +53,6 @@ Section Zn2Z. | WW xh xl => w_to_Z xh * wB + w_to_Z xl end. - Definition interp_carry sign B (interp:znz -> Z) c := - match c with - | C0 x => interp x - | C1 x => sign*B + interp x - end. - End Zn2Z. Implicit Arguments W0 [znz]. |