diff options
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/BinNums.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v index 7b6740e94b..ef2c688759 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -29,6 +29,10 @@ Bind Scope positive_scope with positive. Arguments xO _%positive. Arguments xI _%positive. +Register xI as num.pos.xI. +Register xO as num.pos.xO. +Register xH as num.pos.xH. + (** [N] is a datatype representing natural numbers in a binary way, by extending the [positive] datatype with a zero. Numbers in [N] will also be denoted using a decimal notation; @@ -43,6 +47,10 @@ Delimit Scope N_scope with N. Bind Scope N_scope with N. Arguments Npos _%positive. +Register N as num.N.type. +Register N0 as num.N.N0. +Register Npos as num.N.Npos. + (** [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 @@ -60,3 +68,8 @@ Delimit Scope Z_scope with Z. Bind Scope Z_scope with Z. Arguments Zpos _%positive. Arguments Zneg _%positive. + +Register Z as num.Z.type. +Register Z0 as num.Z.Z0. +Register Zpos as num.Z.Zpos. +Register Zneg as num.Z.Zneg. |