diff options
| author | letouzey | 2011-06-20 17:18:39 +0000 |
|---|---|---|
| committer | letouzey | 2011-06-20 17:18:39 +0000 |
| commit | ca96d3477993d102d6cc42166eab52516630d181 (patch) | |
| tree | 073b17efe149637da819caf527b23cf09f15865d /theories/Numbers/Integer/Abstract | |
| parent | ca1848177a50e51bde0736e51f506e06efc81b1d (diff) | |
Arithemtic: more concerning compare, eqb, leb, ltb
Start of a uniform treatment of compare, eqb, leb, ltb:
- We now ensure that they are provided by N,Z,BigZ,BigN,Nat and Pos
- Some generic properties are derived in OrdersFacts.BoolOrderFacts
In BinPos, more work about sub_mask with nice implications
on compare (e.g. simplier proof of lt_trans).
In BinNat/BinPos, for uniformity, compare_antisym is now
(y ?= x) = CompOpp (x ?=y) instead of the symmetrical result.
In BigN / BigZ, eq_bool is now eqb
In BinIntDef, gtb and geb are kept for the moment, but
a comment advise to rather use ltb and leb. Z.div now uses
Z.ltb and Z.leb.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14227 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer/Abstract')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAxioms.v | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index 237ac93ef5..a5be98aab0 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -111,14 +111,12 @@ Module Type ZQuot' (Z:ZAxiomsMiniSig) := QuotRem' Z <+ QuotRemSpec Z. (** Let's group everything *) -Module Type ZAxiomsSig := - ZAxiomsMiniSig <+ HasCompare <+ HasEqBool <+ HasAbs <+ HasSgn - <+ NZParity.NZParity +Module Type ZAxiomsSig := ZAxiomsMiniSig <+ OrderFunctions + <+ HasAbs <+ HasSgn <+ NZParity.NZParity <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd <+ ZDiv <+ ZQuot <+ NZBits.NZBits. -Module Type ZAxiomsSig' := - ZAxiomsMiniSig' <+ HasCompare <+ HasEqBool <+ HasAbs <+ HasSgn - <+ NZParity.NZParity +Module Type ZAxiomsSig' := ZAxiomsMiniSig' <+ OrderFunctions' + <+ HasAbs <+ HasSgn <+ NZParity.NZParity <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd' <+ ZDiv' <+ ZQuot' <+ NZBits.NZBits'. |