aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/ExtendedBaseVector.v
Commit message (Expand)AuthorAge
* Put ModularBaseSystem carries in terms of [carry_gen], and pushed this change...Gravatar jadep2016-07-25
* Absolutize some importsGravatar Jason Gross2016-07-20
* Remove dependency of ext_base on pseudomersenneGravatar Jason Gross2016-07-20
* Use a proof that doesn't require as many assumptions in extended_base_lengthGravatar Jason Gross2016-07-20
* Remove stuff from PseudoMersenneBaseParamProofs.vGravatar Jason Gross2016-07-19
* Move two_k_nonzero to PseudoMersenneBaseParamProofs.vGravatar Jason Gross2016-07-19
* ext_base: now defined in terms of ext_limb_widthsGravatar Jason Gross2016-07-18
* Move more proofs earlierGravatar Jason Gross2016-07-18
* rewrote Testbit and factored out some necessary lemmas about 'uniform' bases ...Gravatar jadep2016-07-18
* Make [base] and [log_cap] notationsGravatar Jason Gross2016-07-11
* remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
* made BaseVector instance globalGravatar Jade Philipoom2016-03-20
* refactor of Basesystem and ModularBaseSystem; includes general code organizat...Gravatar Jade Philipoom2016-03-20