diff options
Diffstat (limited to 'theories/Numbers/BinNums.v')
| -rw-r--r-- | theories/Numbers/BinNums.v | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v index f8b3d9e1..3ba9d1f5 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -12,13 +12,11 @@ Set Implicit Arguments. -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)] *) + Numbers in [positive] will also be denoted using a decimal notation; + e.g. [6%positive] will abbreviate [xO (xI xH)] *) Inductive positive : Set := | xI : positive -> positive @@ -32,8 +30,8 @@ Arguments xI _%positive. (** [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))] *) + Numbers in [N] will also be denoted using a decimal notation; + e.g. [6%N] will abbreviate [Npos (xO (xI xH))] *) Inductive N : Set := | N0 : N @@ -47,8 +45,8 @@ Arguments Npos _%positive. 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))] *) + Numbers in [Z] will also be denoted using a decimal notation; + e.g. [(-6)%Z] will abbreviate [Zneg (xO (xI xH))] *) Inductive Z : Set := | Z0 : Z |