diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2015-11-20 03:29:09 -0500 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2015-11-20 03:29:09 -0500 |
| commit | dc562d8bf9596fde07e3e3242f345c93c460982a (patch) | |
| tree | 61e9aa013e98a426a7f7815e05af22444bcb6d65 /src/Galois/BaseSystem.v | |
| parent | 545e521740d69724430909e8a1b9059b957ed13d (diff) | |
ModularBaseSystem: relocated base_succ to PsuedoMersenneBaseParams, proved carry_rep.
Diffstat (limited to 'src/Galois/BaseSystem.v')
| -rw-r--r-- | src/Galois/BaseSystem.v | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index f09f87eb6..ead4f9d78 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -17,10 +17,6 @@ Module Type BaseCoefs. Parameter base : list Z. Axiom base_positive : forall b, In b base -> b > 0. (* nonzero would probably work too... *) Axiom b0_1 : forall x, nth_default x base 0 = 1. - Axiom base_succ : forall i, ((S i) < length base)%nat -> - let b := nth_default 0 base in - let r := (b (S i) / b i) in - b (S i) = r * b i. Axiom base_good : forall i j, (i+j < length base)%nat -> let b := nth_default 0 base in |