aboutsummaryrefslogtreecommitdiff
path: root/src/Spec/ModularArithmetic.v
Commit message (Expand)AuthorAge
* Finish absolutizing importsGravatar Jason Gross2016-06-22
* update F Coercions and tutorialGravatar Andres Erbsen2016-06-22
* prove existance of F inv, implement pow -- CompleteEdwardsCurve.unifiedAdd Cl...Gravatar Andres Erbsen2016-06-22
* implement F_oppGravatar Andres Erbsen2016-06-22
* Define F m, a replacement for GF with several benefits.Gravatar Andres Erbsen2016-06-22
* fresh take at specifications using implicit arguments instead of module param...Gravatar Andres Erbsen2016-06-22