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/Numbers/BinNums.v  | 61 +++++++++++++++++++++++++++++++++++++++++++++
 theories/Numbers/vo.itarget |  1 +
 2 files changed, 62 insertions(+)
 create mode 100644 theories/Numbers/BinNums.v

(limited to 'theories/Numbers')

diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v
new file mode 100644
index 0000000000..69754f144a
--- /dev/null
+++ b/theories/Numbers/BinNums.v
@@ -0,0 +1,61 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Binary Numerical Datatypes *)
+
+Set Implicit Arguments.
+(* For compatibility, we will not use generic equality functions *)
+Local Unset Boolean Equality Schemes.
+
+Declare ML Module "z_syntax_plugin".
+
+(** [positive] is a datatype representing the strictly positive integers
+   in a binary way. Starting from 1 (represented by [xH]), one can
+   add a new least significant digit via [xO] (digit 0) or [xI] (digit 1).
+   Numbers in [positive] can also be denoted using a decimal notation;
+   e.g. [6%positive] abbreviates [xO (xI xH)] *)
+
+Inductive positive : Set :=
+  | xI : positive -> positive
+  | xO : positive -> positive
+  | xH : positive.
+
+Delimit Scope positive_scope with positive.
+Bind Scope positive_scope with positive.
+Arguments Scope xO [positive_scope].
+Arguments Scope xI [positive_scope].
+
+(** [N] is a datatype representing natural numbers in a binary way,
+    by extending the [positive] datatype with a zero.
+    Numbers in [N] can also be denoted using a decimal notation;
+    e.g. [6%N] abbreviates [Npos (xO (xI xH))] *)
+
+Inductive N : Set :=
+  | N0 : N
+  | Npos : positive -> N.
+
+Delimit Scope N_scope with N.
+Bind Scope N_scope with N.
+Arguments Scope Npos [positive_scope].
+
+(** [Z] is a datatype representing the integers in a binary way.
+    An integer is either zero or a strictly positive number
+    (coded as a [positive]) or a strictly negative number
+    (whose opposite is stored as a [positive] value).
+    Numbers in [Z] can also be denoted using a decimal notation;
+    e.g. [(-6)%Z] abbreviates [Zneg (xO (xI xH))] *)
+
+Inductive Z : Set :=
+  | Z0 : Z
+  | Zpos : positive -> Z
+  | Zneg : positive -> Z.
+
+Delimit Scope Z_scope with Z.
+Bind Scope Z_scope with Z.
+Arguments Scope Zpos [positive_scope].
+Arguments Scope Zneg [positive_scope].
diff --git a/theories/Numbers/vo.itarget b/theories/Numbers/vo.itarget
index baefbd252a..c69af03fc0 100644
--- a/theories/Numbers/vo.itarget
+++ b/theories/Numbers/vo.itarget
@@ -1,3 +1,4 @@
+BinNums.vo
 BigNumPrelude.vo
 Cyclic/Abstract/CyclicAxioms.vo
 Cyclic/Abstract/NZCyclic.vo
-- 
cgit v1.2.3