aboutsummaryrefslogtreecommitdiff
path: root/src/Spec/ModularArithmetic.v
Commit message (Expand)AuthorAge
* Import prim token notations before using themGravatar Jason Gross2018-08-24
* enforce use of [F.zero], [F.one]; prove Ed25519 admitsGravatar Andres Erbsen2017-07-07
* rename-everythingGravatar Andres Erbsen2017-04-06
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* ModularArithmetic: conversions between [F] and [nat]Gravatar Andres Erbsen2016-09-16
* [cbv beta] in the beginning of Obligation Tactic for 8.5Gravatar Andres Erbsen2016-08-08
* [F] has its own module nowGravatar Andres Erbsen2016-08-05
* Refactor ModularArithmetic into Zmod, expand DecidableGravatar Andres Erbsen2016-08-04
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 20:17:29 +0000