aboutsummaryrefslogtreecommitdiff
path: root/src/Spec/MxDH.v
Commit message (Collapse)AuthorAge
* Support destructuring dlet and sletGravatar Jason Gross2017-05-13
| | | | | The current way to support it is a kludge around the fact that `x binder` only works for recursive notations
* Add commented out proof of equivalence in MxDHGravatar Jason Gross2017-04-12
|
* rename-everythingGravatar Andres Erbsen2017-04-06
|
* Add ladderstep_other_assocGravatar Jason Gross2017-01-07
|
* Add more generic ladderstepGravatar Jason Gross2017-01-07
|
* implement X25519Gravatar Andres Erbsen2016-11-06
|
* MxDH: do not depend on implicit import of list notationsGravatar Andres Erbsen2016-09-26
|
* add Montgomery x-coordinate Diffie-Hellman and Curve25519Gravatar Andres Erbsen2016-09-26