diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-20 17:18:39 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-20 17:18:39 +0000 |
| commit | ca96d3477993d102d6cc42166eab52516630d181 (patch) | |
| tree | 073b17efe149637da819caf527b23cf09f15865d /theories/Numbers/Natural/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/Natural/Abstract')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAxioms.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index 09438628d..45a2cf3e1 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -32,11 +32,11 @@ End NDivSpecific. (** We now group everything together. *) -Module Type NAxiomsSig := NAxiomsMiniSig <+ HasCompare <+ HasEqBool +Module Type NAxiomsSig := NAxiomsMiniSig <+ OrderFunctions <+ NZParity.NZParity <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd <+ NZDiv.NZDiv <+ NZBits.NZBits. -Module Type NAxiomsSig' := NAxiomsMiniSig' <+ HasCompare <+ HasEqBool +Module Type NAxiomsSig' := NAxiomsMiniSig' <+ OrderFunctions' <+ NZParity.NZParity <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd' <+ NZDiv.NZDiv' <+ NZBits.NZBits'. |