diff options
author | Robert Sloan <varomodt@dhcp-18-189-51-40.dyn.MIT.EDU> | 2015-09-10 18:52:17 -0400 |
---|---|---|
committer | Robert Sloan <varomodt@dhcp-18-189-51-40.dyn.MIT.EDU> | 2015-09-10 18:52:17 -0400 |
commit | 2c7b377febf9f42de6c7313dfe4154efdfb90da1 (patch) | |
tree | 3cd619d157fd7d228a9f534be23b3d23261bdf33 /src/Curves/Curve25519.v | |
parent | f4e1d24da03c54fde2df41aa4a3d8ed17940004e (diff) |
init our centralized repo
Diffstat (limited to 'src/Curves/Curve25519.v')
-rw-r--r-- | src/Curves/Curve25519.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v new file mode 100644 index 000000000..8bc3d6e20 --- /dev/null +++ b/src/Curves/Curve25519.v @@ -0,0 +1,13 @@ + +Require Import ZModulo. +(** + * The relevant module is ZModulo: + * the constructor you want is of_pos + * the operations you want are in zmod_ops + * the tactics you want are somewhere between Field and CyclicType: + * probs you want to be converting to/from Z pretty frequently + * + * Coq Reference page: + * https://coq.inria.fr/library/Coq.Numbers.Cyclic.ZModulo.ZModulo.html + *) + |