diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-17 13:33:17 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-17 13:33:17 -0400 |
| commit | 39ec94341fa3a30d97d4462e9c9d481ada2c8d3d (patch) | |
| tree | f9c8fddea0a0fae58172c6f012d368df084f0e1d /src/Spec | |
| parent | 26640780a5cdce3aed531c1bf7cdaa692244edc7 (diff) | |
move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems
Diffstat (limited to 'src/Spec')
| -rw-r--r-- | src/Spec/CompleteEdwardsCurve.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 518d3d551..5df36e295 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -8,11 +8,11 @@ Module E. * <https://eprint.iacr.org/2015/677.pdf> *) - Context {F eq Fzero one opp Fadd sub Fmul inv div} `{Algebra.field F eq Fzero one opp Fadd sub Fmul inv div}. - Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. - Local Notation "0" := Fzero. Local Notation "1" := one. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} `{Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}. + Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Notation "0" := Fzero. Local Notation "1" := Fone. Local Infix "+" := Fadd. Local Infix "*" := Fmul. - Local Infix "-" := sub. Local Infix "/" := div. + Local Infix "-" := Fsub. Local Infix "/" := Fdiv. Local Notation "x ^2" := (x*x) (at level 30). Context {a d: F}. |