diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-12 23:40:15 -0500 |
|---|---|---|
| committer |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:39:04 -0400 |
| commit | d2b44152fa01a7143b1811e540daf7696a4d40e1 (patch) | |
| tree | d0d79064f664b1f60df38952bb3a8756dd35d70a /src/Spec/ModularArithmetic.v | |
| parent | 67004987959e1c9e46e879f06da00d567547482e (diff) | |
implement F_opp
Diffstat (limited to 'src/Spec/ModularArithmetic.v')
| -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. |