aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Natural/Abstract/NProperties.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NProperties.v')
-rw-r--r--theories/Numbers/Natural/Abstract/NProperties.v21
1 files changed, 16 insertions, 5 deletions
diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v
index 907394101..df3e7c7e4 100644
--- a/theories/Numbers/Natural/Abstract/NProperties.v
+++ b/theories/Numbers/Natural/Abstract/NProperties.v
@@ -9,9 +9,20 @@
Require Export NAxioms.
Require Import NMaxMin NParity NPow NSqrt NLog NDiv NGcd NLcm NBits.
-(** This functor summarizes all known facts about N. *)
+(** The two following functors summarize all known facts about N.
-Module Type NProp (N:NAxiomsSig) :=
- NMaxMinProp N <+ NParityProp N <+ NPowProp N <+ NSqrtProp N
- <+ NLog2Prop N <+ NDivProp N <+ NGcdProp N <+ NLcmProp N
- <+ NBitsProp N.
+ - [NBasicProp] provides properties of basic functions:
+ + - * min max <= <
+
+ - [NExtraProp] provides properties of advanced functions:
+ pow, sqrt, log2, div, gcd, and bitwise functions.
+
+ If necessary, the earlier all-in-one functor [NProp]
+ could be re-obtained via [NBasicProp <+ NExtraProp] *)
+
+Module Type NBasicProp (N:NAxiomsMiniSig) := NMaxMinProp N.
+
+Module Type NExtraProp (N:NAxiomsSig)(P:NBasicProp N) :=
+ NParityProp N P <+ NPowProp N P <+ NSqrtProp N P
+ <+ NLog2Prop N P <+ NDivProp N P <+ NGcdProp N P <+ NLcmProp N P
+ <+ NBitsProp N P.