diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-07-28 18:40:28 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-08-04 11:47:51 -0400 |
| commit | 4964f1ff2d40ba08573deddca56140c4ac4b19eb (patch) | |
| tree | 61b24623e414dfa3e09a32cf62e8acd1909dae37 /src/Spec/WeierstrassCurve.v | |
| parent | fbb0f64892560322ed9dcd0f664e730e74de9b4e (diff) | |
Refactor ModularArithmetic into Zmod, expand Decidable
ModularArithmetic now uses Algebra lemmas in various places instead of
custom manual proofs. Similarly, Util.Decidable is used to state and
prove the relevant decidability results.
Backwards-incompatible changes:
F_some_lemma -> Zmod.some_lemma
Arguments ZToField _%Z _%Z : clear implicits.
inv_spec says inv x * x = 1, not x * inv x = 1
Diffstat (limited to 'src/Spec/WeierstrassCurve.v')
| -rw-r--r-- | src/Spec/WeierstrassCurve.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v index 7ec5d99ec..e2c99a8fe 100644 --- a/src/Spec/WeierstrassCurve.v +++ b/src/Spec/WeierstrassCurve.v @@ -11,8 +11,8 @@ Module E. 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 Infix "=?" := Algebra.eq_dec (at level 70, no associativity) : type_scope. - Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Algebra.eq_dec x y)) : bool_scope. + Local Notation "x =? y" := (Decidable.dec (Feq x y)) (at level 70, no associativity) : type_scope. + Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Decidable.dec (Feq x y))) : bool_scope. Local Infix "+" := Fadd. Local Infix "*" := Fmul. Local Infix "-" := Fsub. Local Infix "/" := Fdiv. Local Notation "- x" := (Fopp x). |