aboutsummaryrefslogtreecommitdiff
path: root/src/Encoding/ModularWordEncodingTheorems.v
Commit message (Expand)AuthorAge
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* [F] has its own module nowGravatar Andres Erbsen2016-08-05
* address code review commentsGravatar Andres Erbsen2016-08-04
* Refactor ModularArithmetic into Zmod, expand DecidableGravatar Andres Erbsen2016-08-04
* Make ZUtil more uniformGravatar Jason Gross2016-07-02
* remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
* Moved sign_bit definition to Spec.Gravatar jadep2016-04-29
* Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener...Gravatar jadep2016-04-28
* Completed encoding reorganization; factored sign_bit out of PointEncodings an...Gravatar jadep2016-04-28