From f61a557fbbdb89a4c24a8050a67252c3ecda6ea7 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:09 +0000 Subject: Definitions of positive, N, Z moved in Numbers/BinNums.v In the coming reorganisation, the name Z in BinInt will be a module containing all code and properties about binary integers. The inductive type Z hence cannot be at the same location. Same for N and positive. Apart for this naming constraint, it also have advantages : presenting the three types at once is clearer, and we will be able to refer to N in BinPos (for instance for output type of a predecessor function on positive). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14097 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/PArith/BinPos.v | 40 +++++++++++++++++----------------------- theories/PArith/PArith.v | 2 +- 2 files changed, 18 insertions(+), 24 deletions(-) (limited to 'theories/PArith') 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. -- cgit v1.2.3