diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-07-06 12:45:20 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-07-06 12:45:20 -0400 |
| commit | e4bbfc3ba802d6a8fc1eca47da5202b22b1decaf (patch) | |
| tree | 7dff9a955b5b53f8ad79f966b4794efb9eab7700 /_CoqProject | |
| parent | e215871febb7d1294aa5aa13b0c70b2207e745e2 (diff) | |
Factored out some proofs that rely only on base being powers of two, and defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util.
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 904d716b8..55973017b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -37,6 +37,8 @@ src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/ModularBaseSystem.v src/ModularArithmetic/ModularBaseSystemOpt.v src/ModularArithmetic/ModularBaseSystemProofs.v +src/ModularArithmetic/Pow2Base.v +src/ModularArithmetic/Pow2BaseProofs.v src/ModularArithmetic/Pre.v src/ModularArithmetic/PrimeFieldTheorems.v src/ModularArithmetic/PseudoMersenneBaseParamProofs.v |