diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-22 13:54:20 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-22 13:54:20 -0700 |
| commit | a4c50ceb1c773c8b1f36a5409c2112cf80725f7e (patch) | |
| tree | 50f362f2dfa93bc4cb72034a0a1c42750a8af65d /src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | |
| parent | 585e947def4cce90241a361032344e323e15d48b (diff) | |
Fix broken notations (hopefully)
Diffstat (limited to 'src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v')
| -rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index c217303aa..476592b36 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -19,7 +19,7 @@ Module E. Local Notation "0" := Fzero. Local Notation "1" := Fone. Local Infix "+" := Fadd. Local Infix "*" := Fmul. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. - Local Notation "x ^2" := (x*x). + Local Notation "x ^ 2" := (x*x). Local Notation point := (@point F Feq Fone Fadd Fmul a d). Local Notation onCurve := (@onCurve F Feq Fone Fadd Fmul a d). @@ -159,7 +159,7 @@ Module E. Admitted. Section PointCompression. - Local Notation "x ^2" := (x*x). + Local Notation "x ^ 2" := (x*x). Definition solve_for_x2 (y : F) := ((y^2 - 1) / (d * (y^2) - a)). Lemma a_d_y2_nonzero : forall y, d * y^2 - a <> 0. |