diff options
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Decimal.v | 5 | ||||
| -rw-r--r-- | theories/Init/Prelude.v | 2 |
2 files changed, 5 insertions, 2 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/Init/Prelude.v b/theories/Init/Prelude.v index 5e29f854e8..81268a87ad 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -38,7 +38,7 @@ Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int : dec_int_scope. (* Parsing / printing of [nat] numbers *) -Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000). +Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5001). (* Printing/Parsing of bytes *) Export Byte.ByteSyntaxNotations. |