diff options
| author | Vincent Laporte | 2018-10-12 12:22:43 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-01-25 08:22:25 +0000 |
| commit | 68304575dd3fd85d26e2f1bdff84721df8481952 (patch) | |
| tree | f6d142e1d95740aed8fa1825bb15ea3131484e19 /theories | |
| parent | 6994539744e4ffaa4f622c8bccc66276e445ae9a (diff) | |
[Numeral notations] Use Coqlib registered constants
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/Decimal.v | 5 | ||||
| -rw-r--r-- | theories/Numbers/BinNums.v | 1 |
2 files changed, 5 insertions, 1 deletions
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 537400fb05..3d4b3d0568 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -40,7 +40,7 @@ Notation zero := (D0 Nil). (** For signed integers, we use two constructors [Pos] and [Neg]. *) -Inductive int := Pos (d:uint) | Neg (d:uint). +Variant int := Pos (d:uint) | Neg (d:uint). Declare Scope dec_uint_scope. Delimit Scope dec_uint_scope with uint. @@ -50,6 +50,9 @@ Declare Scope dec_int_scope. Delimit Scope dec_int_scope with int. Bind Scope dec_int_scope with int. +Register uint as num.uint.type. +Register int as num.int.type. + (** This representation favors simplicity over canonicity. For normalizing numbers, we need to remove head zero digits, and choose our canonical representation of 0 (here [D0 Nil] diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v index ef2c688759..247827597a 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -29,6 +29,7 @@ Bind Scope positive_scope with positive. Arguments xO _%positive. Arguments xI _%positive. +Register positive as num.pos.type. Register xI as num.pos.xI. Register xO as num.pos.xO. Register xH as num.pos.xH. |