aboutsummaryrefslogtreecommitdiff
path: root/src/Spec/ModularArithmetic.v
Commit message (Expand)AuthorAge
* compute on [F q]!Gravatar Andres Erbsen2016-07-20
* More changes for 8.5Gravatar Jason Gross2016-06-10
* Finish absolutizing importsGravatar Jason Gross2016-03-10
* update F Coercions and tutorialGravatar Andres Erbsen2016-02-14
* prove existance of F inv, implement pow -- CompleteEdwardsCurve.unifiedAdd Cl...Gravatar Andres Erbsen2016-02-13
* implement F_oppGravatar Andres Erbsen2016-02-12
* Define F m, a replacement for GF with several benefits.Gravatar Andres Erbsen2016-02-11
* fresh take at specifications using implicit arguments instead of module param...Gravatar Andres Erbsen2016-02-07