aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/Pow2Base.v
Commit message (Expand)AuthorAge
* Fully qualify [Require]sGravatar Jason Gross2016-09-08
* mergeGravatar jadep2016-08-11
|\
| * Add carry_simple_subGravatar Jason Gross2016-08-10
* | Made decode_bitwise proofs go away, and proved sane lemmas about Z.testbit (B...Gravatar jadep2016-08-10
|/
* Put ModularBaseSystem carries in terms of [carry_gen], and pushed this change...Gravatar jadep2016-07-25
* Changed name of [carry_and_reduce_single] to [carry_single], since it does no...Gravatar jadep2016-07-21
* re-introduced extra field isomorphism layer for 8.4 compatibility and better ...Gravatar jadep2016-07-21
* Use update_nth in add_to_nth (#26)Gravatar Jason Gross2016-07-19
* Express carry_simple in terms of carry_genGravatar Jason Gross2016-07-18
* Move some definitions to Pow2Base (#24)Gravatar Jason Gross2016-07-18
* Make [base] and [log_cap] notationsGravatar Jason Gross2016-07-11
* Factored out some proofs that rely only on base being powers of two, and defi...Gravatar jadep2016-07-06