diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-04-22 15:27:42 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-04-22 15:27:42 -0400 |
| commit | 2b43845eabdb5522162d52a86ecf6dfaf6dbc847 (patch) | |
| tree | 00c193d89adbd22bac516072164b76f363241d9e /src/Spec/CompleteEdwardsCurve.v | |
| parent | 30ef733d1a5820456d5e5aac774270b51a9c9dde (diff) | |
point_eq_dec
Diffstat (limited to 'src/Spec/CompleteEdwardsCurve.v')
| -rw-r--r-- | src/Spec/CompleteEdwardsCurve.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index b7d2c0d8e..8dbfdf7b9 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -46,11 +46,8 @@ Section TwistedEdwardsCurves. | O => zero | S n' => unifiedAdd P (scalarMult n' P) end. - - Axiom point_eq_dec : forall P Q : point, {P = Q} + {P <> Q}. End TwistedEdwardsCurves. Delimit Scope E_scope with E. Infix "+" := unifiedAdd : E_scope. -Infix "*" := scalarMult : E_scope. -Infix "==" := point_eq_dec (no associativity, at level 70) : E_scope. +Infix "*" := scalarMult : E_scope.
\ No newline at end of file |