aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/Pow2Base.v
Commit message (Expand)AuthorAge
* 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