diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-07-11 17:38:21 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-07-11 17:44:40 -0400 |
| commit | 29579220a48248d2e206880fc59089a19a4d4885 (patch) | |
| tree | 9588f475281630ff33c2dcef1aec9b232672df7b /src/ModularArithmetic/ExtendedBaseVector.v | |
| parent | bb38344557cddbc64eac0eb5b174d54c0507e08a (diff) | |
Make [base] and [log_cap] notations
Also use [ZUtil.Z.pow2_mod]. This lets us remove the dependency of
ModularBaseSystem on ModularArithmetic.PseudoMersenneBaseParamProofs.
This is a small part of reorganizing and factoring ModularBaseSystem for
use with Barrett reduction.
Diffstat (limited to 'src/ModularArithmetic/ExtendedBaseVector.v')
| -rw-r--r-- | src/ModularArithmetic/ExtendedBaseVector.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v index 9ed7d065e..2a06d9c41 100644 --- a/src/ModularArithmetic/ExtendedBaseVector.v +++ b/src/ModularArithmetic/ExtendedBaseVector.v @@ -9,6 +9,7 @@ Local Open Scope Z_scope. Section ExtendedBaseVector. Context `{prm : PseudoMersenneBaseParams}. + Local Notation base := (Pow2Base.base_from_limb_widths limb_widths). (* This section defines a new BaseVector that has double the length of the BaseVector * used to construct [params]. The coefficients of the new vector are as follows: @@ -159,4 +160,3 @@ Section ExtendedBaseVector. unfold ext_base; rewrite app_length; rewrite map_length; auto. Qed. End ExtendedBaseVector. - |