diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-12 23:40:15 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-02-12 23:40:15 -0500 |
| commit | 33923317a143904a1bdd52e2664a210e344a4319 (patch) | |
| tree | 7e0821651ffde23e311ea68ed6b9d0024032d495 /src/Spec | |
| parent | 6c993ee91855ee8c19c292cd164ab24a7c1012f8 (diff) | |
implement F_opp
Diffstat (limited to 'src/Spec')
| -rw-r--r-- | src/Spec/ModularArithmetic.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v index e2243dfff..2f887548f 100644 --- a/src/Spec/ModularArithmetic.v +++ b/src/Spec/ModularArithmetic.v @@ -31,8 +31,8 @@ Section FieldOperations. Definition add (a b:Fm) : Fm := ZToField (a + b). Definition mul (a b:Fm) : Fm := ZToField (a * b). - Parameter opp : Fm -> Fm. - Axiom F_opp_spec : forall (a:Fm), add a (opp a) = 0. + Definition opp_with_spec : { opp | forall x, add x (opp x) = 0 } := Pre.opp_impl. + Definition opp : F m -> F m := Eval hnf in proj1_sig opp_with_spec. Definition sub (a b:Fm) : Fm := add a (opp b). Parameter inv : Fm -> Fm. |