diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-06-20 15:07:03 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-06-20 15:07:03 -0400 |
commit | 0ae5f6871b29d20f48b5df6dab663b5a44162d01 (patch) | |
tree | 33b11090af2555a91a593f9b919edf83c71557cd /src/Spec/CompleteEdwardsCurve.v | |
parent | a0bdb14300aa57eed684992a23a57fd319ef97c0 (diff) |
remove trailing whitespace from src/
Diffstat (limited to 'src/Spec/CompleteEdwardsCurve.v')
-rw-r--r-- | src/Spec/CompleteEdwardsCurve.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 5df36e295..88388ee0a 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -24,12 +24,12 @@ Module E. nonsquare_d : forall x, x^2 <> d }. Context `{twisted_edwards_params}. - + Definition point := { P | let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2 }. Definition coordinates (P:point) : (F*F) := proj1_sig P. Program Definition zero : point := (0, 1). - + Program Definition add (P1 P2:point) : point := exist _ ( let (x1, y1) := coordinates P1 in let (x2, y2) := coordinates P2 in @@ -47,7 +47,7 @@ Module E. end. End TwistedEdwardsCurves. End E. - + Delimit Scope E_scope with E. Infix "+" := E.add : E_scope. Infix "*" := E.mul : E_scope.
\ No newline at end of file |