diff options
Diffstat (limited to 'theories/PArith')
-rw-r--r-- | theories/PArith/BinPos.v | 40 | ||||
-rw-r--r-- | theories/PArith/PArith.v | 2 |
2 files changed, 18 insertions, 24 deletions
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index ec18d8dc5..badae225f 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -7,32 +7,20 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Declare ML Module "z_syntax_plugin". +Require Export BinNums. (**********************************************************************) -(** * Binary positive numbers *) +(** * Binary positive numbers, operations and properties *) (**********************************************************************) (** Initial development by Pierre Crégut, CNET, Lannion, France *) -Inductive positive : Set := -| xI : positive -> positive -| xO : positive -> positive -| xH : positive. - -(** Declare binding key for scope positive_scope *) - -Delimit Scope positive_scope with positive. - -(** Automatically open scope positive_scope for type positive, xO and xI *) - -Bind Scope positive_scope with positive. -Arguments Scope xO [positive_scope]. -Arguments Scope xI [positive_scope]. +(** The type [positive] and its constructors [xI] and [xO] and [xH] + are now defined in [BinNums.v] *) (** Postfix notation for positive numbers, allowing to mimic the position of bits in a big-endian representation. - For instance, we can write 1~1~0 instead of (xO (xI xH)) + For instance, we can write [1~1~0] instead of [(xO (xI xH))] for the number 6 (which is 110 in binary notation). *) @@ -42,12 +30,8 @@ Notation "p ~ 0" := (xO p) (at level 7, left associativity, format "p '~' '0'") : positive_scope. Local Open Scope positive_scope. - -(* In the current file, [xH] cannot yet be written as [1], since the - interpretation of positive numerical constants is not available - yet. We fix this here with an ad-hoc temporary notation. *) - -Local Notation "1" := xH (at level 7). +Local Unset Boolean Equality Schemes. +Local Unset Case Analysis Schemes. (**********************************************************************) (** * Operations over positive numbers *) @@ -1599,3 +1583,13 @@ Proof. apply Pmult_le_mono_l. apply Ple_lteq; left. rewrite xI_succ_xO. apply Plt_succ_r, IHp. Qed. + +(** Compatibility notations *) + +Notation positive := positive (only parsing). +Notation positive_rect := positive_rect (only parsing). +Notation positive_rec := positive_rec (only parsing). +Notation positive_ind := positive_ind (only parsing). +Notation xI := xI (only parsing). +Notation xO := xO (only parsing). +Notation xH := xH (only parsing). diff --git a/theories/PArith/PArith.v b/theories/PArith/PArith.v index 8688c5013..e2bec88af 100644 --- a/theories/PArith/PArith.v +++ b/theories/PArith/PArith.v @@ -8,4 +8,4 @@ (** Library for positive natural numbers *) -Require Export BinPos Pnat Pminmax Psqrt Pgcd POrderedType. +Require Export BinNums BinPos Pnat Pminmax Psqrt Pgcd POrderedType. |