Add more constant notations

2 files changed, 112 insertions, 0 deletions

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 7113173f6..e79341ff0 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -25,10 +25,12 @@ nums = tuple(sorted(set(systematic_nums + [
     5311,
     32765,
     65531,
+    65534,
     114687,
     121665,
     130307,
     131039,
+    131062,
     131067,
     261167,
     261575,
@@ -53,11 +55,13 @@ nums = tuple(sorted(set(systematic_nums + [
     1048559,
     1048573,
     1048574,
+    1359870,
     2060031,
     2081439,
     2094335,
     2096127,
     2096128,
+    2097114,
     2097118,
     2097127,
     2097135,
@@ -85,14 +89,18 @@ nums = tuple(sorted(set(systematic_nums + [
     8388605,
     8388606,
     11599871,
+    16647166,
     16711679,
     16775935,
     16776959,
+    16776982,
+    16777162,
     16777189,
     16777191,
     16777199,
     16777201,
     16777207,
+    16777210,
     16777213,
     16777214,
     33423358,
@@ -222,6 +230,7 @@ nums = tuple(sorted(set(systematic_nums + [
     549755813854,
     549755813869,
     549755813886,
+    1099511627566,
     1099511627738,
     1099511627761,
     1099511627774,
@@ -306,6 +315,8 @@ nums = tuple(sorted(set(systematic_nums + [
     2251799813685242,
     2251799813685246,
     2920302883373054,
+    4423885034356734,
+    4469858364293118,
     4497552313417726,
     4503595332402223,
     4503599627368966,
@@ -321,7 +332,10 @@ nums = tuple(sorted(set(systematic_nums + [
     4503599627370494,
     9007190664804446,
     9007199187632127,
+    9007199254739854,
+    9007199254740030,
     9007199254740614,
+    9007199254740618,
     9007199254740963,
     9007199254740982,
     9007199254740988,
@@ -817,6 +831,8 @@ Notation "'0b1000000000000001'" (* 32769 (0x8001) *)
   := (Const WO~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
 Notation "'0b1111111111111011'" (* 65531 (0xfffb) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1).
+Notation "'0b1111111111111110'" (* 65534 (0xfffe) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0b1111111111111111'" (* 65535 (0xffff) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b10000000000000000'" (* 65536 (0x10000) *)
@@ -831,6 +847,8 @@ Notation "'0b11111110100000011'" (* 130307 (0x1fd03) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~1~0~0~0~0~0~0~1~1).
 Notation "'0b11111111111011111'" (* 131039 (0x1ffdf) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1).
+Notation "'0b11111111111110110'" (* 131062 (0x1fff6) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
 Notation "'0b11111111111111011'" (* 131067 (0x1fffb) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1).
 Notation "'0b11111111111111111'" (* 131071 (0x1ffff) *)
@@ -903,6 +921,8 @@ Notation "'0b100000000000000000000'" (* 1048576 (0x100000) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
 Notation "'0b100000000000000000001'" (* 1048577 (0x100001) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0b101001011111111111110'" (* 1359870 (0x14bffe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0b111110110111011111111'" (* 2060031 (0x1f6eff) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~0~1~1~0~1~1~1~0~1~1~1~1~1~1~1~1).
 Notation "'0b111111100001010011111'" (* 2081439 (0x1fc29f) *)
@@ -913,6 +933,8 @@ Notation "'0b111111111101111111111'" (* 2096127 (0x1ffbff) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b111111111110000000000'" (* 2096128 (0x1ffc00) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0).
+Notation "'0b111111111111111011010'" (* 2097114 (0x1fffda) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
 Notation "'0b111111111111111011110'" (* 2097118 (0x1fffde) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
 Notation "'0b111111111111111100111'" (* 2097127 (0x1fffe7) *)
@@ -985,12 +1007,18 @@ Notation "'0b100000000000000000000001'" (* 8388609 (0x800001) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
 Notation "'0b101100001111111111111111'" (* 11599871 (0xb0ffff) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~0~1~1~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0b111111100000001111111110'" (* 16647166 (0xfe03fe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~0).
 Notation "'0b111111101111111111111111'" (* 16711679 (0xfeffff) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b111111111111101011111111'" (* 16775935 (0xfffaff) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1~1~1~1~1~1~1).
 Notation "'0b111111111111111011111111'" (* 16776959 (0xfffeff) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1).
+Notation "'0b111111111111111100010110'" (* 16776982 (0xffff16) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0~1~1~0).
+Notation "'0b111111111111111111001010'" (* 16777162 (0xffffca) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~0).
 Notation "'0b111111111111111111100101'" (* 16777189 (0xffffe5) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1).
 Notation "'0b111111111111111111100111'" (* 16777191 (0xffffe7) *)
@@ -1001,6 +1029,8 @@ Notation "'0b111111111111111111110001'" (* 16777201 (0xfffff1) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1).
 Notation "'0b111111111111111111110111'" (* 16777207 (0xfffff7) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1).
+Notation "'0b111111111111111111111010'" (* 16777210 (0xfffffa) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
 Notation "'0b111111111111111111111101'" (* 16777213 (0xfffffd) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1).
 Notation "'0b111111111111111111111110'" (* 16777214 (0xfffffe) *)
@@ -1353,6 +1383,8 @@ Notation "'0b1000000000000000000000000000000000000000'" (* 549755813888 (0x80000
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
 Notation "'0b1000000000000000000000000000000000000001'" (* 549755813889 (0x8000000001) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0b1111111111111111111111111111111100101110'" (* 1099511627566 (0xffffffff2e) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~1~0).
 Notation "'0b1111111111111111111111111111111111011010'" (* 1099511627738 (0xffffffffda) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
 Notation "'0b1111111111111111111111111111111111110001'" (* 1099511627761 (0xfffffffff1) *)
@@ -1593,6 +1625,10 @@ Notation "'0b1000000000000000000000000000000000000000000000000001'" (* 225179981
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
 Notation "'0b1010010111111111111111111111111111111111111111111110'" (* 2920302883373054 (0xa5ffffffffffe) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
+Notation "'0b1111101101110111111111111111111111111111111111111110'" (* 4423885034356734 (0xfb77ffffffffe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~0~1~1~0~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
+Notation "'0b1111111000010100111111111111111111111111111111111110'" (* 4469858364293118 (0xfe14ffffffffe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~0~0~0~1~0~1~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0b1111111110100111111111111111111111111111111111111110'" (* 4497552313417726 (0xffa7ffffffffe) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~0~1~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0b1111111111111111111011111111111111111111110000101111'" (* 4503595332402223 (0xffffefffffc2f) *)
@@ -1629,8 +1665,14 @@ Notation "'0b11111111111111111110111111111111111111111100001011110'" (* 90071906
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1~0).
 Notation "'0b11111111111111111111111111011111111111111111111111111'" (* 9007199187632127 (0x1ffffffbffffff) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0b11111111111111111111111111111111111111111101110001110'" (* 9007199254739854 (0x1ffffffffffb8e) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1~0).
+Notation "'0b11111111111111111111111111111111111111111110000111110'" (* 9007199254740030 (0x1ffffffffffc3e) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1~0).
 Notation "'0b11111111111111111111111111111111111111111111010000110'" (* 9007199254740614 (0x1ffffffffffe86) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~1~1~0).
+Notation "'0b11111111111111111111111111111111111111111111010001010'" (* 9007199254740618 (0x1ffffffffffe8a) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~1~0~1~0).
 Notation "'0b11111111111111111111111111111111111111111111111100011'" (* 9007199254740963 (0x1fffffffffffe3) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~1).
 Notation "'0b11111111111111111111111111111111111111111111111110110'" (* 9007199254740982 (0x1ffffffffffff6) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 807910f7d..20d24bb66 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -25,10 +25,12 @@ nums = tuple(sorted(set(systematic_nums + [
     5311,
     32765,
     65531,
+    65534,
     114687,
     121665,
     130307,
     131039,
+    131062,
     131067,
     261167,
     261575,
@@ -53,11 +55,13 @@ nums = tuple(sorted(set(systematic_nums + [
     1048559,
     1048573,
     1048574,
+    1359870,
     2060031,
     2081439,
     2094335,
     2096127,
     2096128,
+    2097114,
     2097118,
     2097127,
     2097135,
@@ -85,14 +89,18 @@ nums = tuple(sorted(set(systematic_nums + [
     8388605,
     8388606,
     11599871,
+    16647166,
     16711679,
     16775935,
     16776959,
+    16776982,
+    16777162,
     16777189,
     16777191,
     16777199,
     16777201,
     16777207,
+    16777210,
     16777213,
     16777214,
     33423358,
@@ -222,6 +230,7 @@ nums = tuple(sorted(set(systematic_nums + [
     549755813854,
     549755813869,
     549755813886,
+    1099511627566,
     1099511627738,
     1099511627761,
     1099511627774,
@@ -306,6 +315,8 @@ nums = tuple(sorted(set(systematic_nums + [
     2251799813685242,
     2251799813685246,
     2920302883373054,
+    4423885034356734,
+    4469858364293118,
     4497552313417726,
     4503595332402223,
     4503599627368966,
@@ -321,7 +332,10 @@ nums = tuple(sorted(set(systematic_nums + [
     4503599627370494,
     9007190664804446,
     9007199187632127,
+    9007199254739854,
+    9007199254740030,
     9007199254740614,
+    9007199254740618,
     9007199254740963,
     9007199254740982,
     9007199254740988,
@@ -1145,6 +1159,10 @@ Notation "'0xfffb'" (* 65531 (0xfffb) *)
   := (Const 65531%Z).
 Notation "'0xfffb'" (* 65531 (0xfffb) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1).
+Notation "'0xfffe'" (* 65534 (0xfffe) *)
+  := (Const 65534%Z).
+Notation "'0xfffe'" (* 65534 (0xfffe) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0xffff'" (* 65535 (0xffff) *)
   := (Const 65535%Z).
 Notation "'0xffff'" (* 65535 (0xffff) *)
@@ -1173,6 +1191,10 @@ Notation "'0x1ffdf'" (* 131039 (0x1ffdf) *)
   := (Const 131039%Z).
 Notation "'0x1ffdf'" (* 131039 (0x1ffdf) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1).
+Notation "'0x1fff6'" (* 131062 (0x1fff6) *)
+  := (Const 131062%Z).
+Notation "'0x1fff6'" (* 131062 (0x1fff6) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
 Notation "'0x1fffb'" (* 131067 (0x1fffb) *)
   := (Const 131067%Z).
 Notation "'0x1fffb'" (* 131067 (0x1fffb) *)
@@ -1317,6 +1339,10 @@ Notation "'0x100001'" (* 1048577 (0x100001) *)
   := (Const 1048577%Z).
 Notation "'0x100001'" (* 1048577 (0x100001) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0x14bffe'" (* 1359870 (0x14bffe) *)
+  := (Const 1359870%Z).
+Notation "'0x14bffe'" (* 1359870 (0x14bffe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0x1f6eff'" (* 2060031 (0x1f6eff) *)
   := (Const 2060031%Z).
 Notation "'0x1f6eff'" (* 2060031 (0x1f6eff) *)
@@ -1337,6 +1363,10 @@ Notation "'0x1ffc00'" (* 2096128 (0x1ffc00) *)
   := (Const 2096128%Z).
 Notation "'0x1ffc00'" (* 2096128 (0x1ffc00) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0).
+Notation "'0x1fffda'" (* 2097114 (0x1fffda) *)
+  := (Const 2097114%Z).
+Notation "'0x1fffda'" (* 2097114 (0x1fffda) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
 Notation "'0x1fffde'" (* 2097118 (0x1fffde) *)
   := (Const 2097118%Z).
 Notation "'0x1fffde'" (* 2097118 (0x1fffde) *)
@@ -1481,6 +1511,10 @@ Notation "'0xb0ffff'" (* 11599871 (0xb0ffff) *)
   := (Const 11599871%Z).
 Notation "'0xb0ffff'" (* 11599871 (0xb0ffff) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~0~1~1~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0xfe03fe'" (* 16647166 (0xfe03fe) *)
+  := (Const 16647166%Z).
+Notation "'0xfe03fe'" (* 16647166 (0xfe03fe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~0).
 Notation "'0xfeffff'" (* 16711679 (0xfeffff) *)
   := (Const 16711679%Z).
 Notation "'0xfeffff'" (* 16711679 (0xfeffff) *)
@@ -1493,6 +1527,14 @@ Notation "'0xfffeff'" (* 16776959 (0xfffeff) *)
   := (Const 16776959%Z).
 Notation "'0xfffeff'" (* 16776959 (0xfffeff) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1).
+Notation "'0xffff16'" (* 16776982 (0xffff16) *)
+  := (Const 16776982%Z).
+Notation "'0xffff16'" (* 16776982 (0xffff16) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0~1~1~0).
+Notation "'0xffffca'" (* 16777162 (0xffffca) *)
+  := (Const 16777162%Z).
+Notation "'0xffffca'" (* 16777162 (0xffffca) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~0).
 Notation "'0xffffe5'" (* 16777189 (0xffffe5) *)
   := (Const 16777189%Z).
 Notation "'0xffffe5'" (* 16777189 (0xffffe5) *)
@@ -1513,6 +1555,10 @@ Notation "'0xfffff7'" (* 16777207 (0xfffff7) *)
   := (Const 16777207%Z).
 Notation "'0xfffff7'" (* 16777207 (0xfffff7) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1).
+Notation "'0xfffffa'" (* 16777210 (0xfffffa) *)
+  := (Const 16777210%Z).
+Notation "'0xfffffa'" (* 16777210 (0xfffffa) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
 Notation "'0xfffffd'" (* 16777213 (0xfffffd) *)
   := (Const 16777213%Z).
 Notation "'0xfffffd'" (* 16777213 (0xfffffd) *)
@@ -2217,6 +2263,10 @@ Notation "'0x8000000001'" (* 549755813889 (0x8000000001) *)
   := (Const 549755813889%Z).
 Notation "'0x8000000001'" (* 549755813889 (0x8000000001) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0xffffffff2e'" (* 1099511627566 (0xffffffff2e) *)
+  := (Const 1099511627566%Z).
+Notation "'0xffffffff2e'" (* 1099511627566 (0xffffffff2e) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~1~0).
 Notation "'0xffffffffda'" (* 1099511627738 (0xffffffffda) *)
   := (Const 1099511627738%Z).
 Notation "'0xffffffffda'" (* 1099511627738 (0xffffffffda) *)
@@ -2697,6 +2747,14 @@ Notation "'0xa5ffffffffffe'" (* 2920302883373054 (0xa5ffffffffffe) *)
   := (Const 2920302883373054%Z).
 Notation "'0xa5ffffffffffe'" (* 2920302883373054 (0xa5ffffffffffe) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
+Notation "'0xfb77ffffffffe'" (* 4423885034356734 (0xfb77ffffffffe) *)
+  := (Const 4423885034356734%Z).
+Notation "'0xfb77ffffffffe'" (* 4423885034356734 (0xfb77ffffffffe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~0~1~1~0~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
+Notation "'0xfe14ffffffffe'" (* 4469858364293118 (0xfe14ffffffffe) *)
+  := (Const 4469858364293118%Z).
+Notation "'0xfe14ffffffffe'" (* 4469858364293118 (0xfe14ffffffffe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~0~0~0~1~0~1~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0xffa7ffffffffe'" (* 4497552313417726 (0xffa7ffffffffe) *)
   := (Const 4497552313417726%Z).
 Notation "'0xffa7ffffffffe'" (* 4497552313417726 (0xffa7ffffffffe) *)
@@ -2769,10 +2827,22 @@ Notation "'0x1ffffffbffffff'" (* 9007199187632127 (0x1ffffffbffffff) *)
   := (Const 9007199187632127%Z).
 Notation "'0x1ffffffbffffff'" (* 9007199187632127 (0x1ffffffbffffff) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0x1ffffffffffb8e'" (* 9007199254739854 (0x1ffffffffffb8e) *)
+  := (Const 9007199254739854%Z).
+Notation "'0x1ffffffffffb8e'" (* 9007199254739854 (0x1ffffffffffb8e) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1~0).
+Notation "'0x1ffffffffffc3e'" (* 9007199254740030 (0x1ffffffffffc3e) *)
+  := (Const 9007199254740030%Z).
+Notation "'0x1ffffffffffc3e'" (* 9007199254740030 (0x1ffffffffffc3e) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1~0).
 Notation "'0x1ffffffffffe86'" (* 9007199254740614 (0x1ffffffffffe86) *)
   := (Const 9007199254740614%Z).
 Notation "'0x1ffffffffffe86'" (* 9007199254740614 (0x1ffffffffffe86) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~1~1~0).
+Notation "'0x1ffffffffffe8a'" (* 9007199254740618 (0x1ffffffffffe8a) *)
+  := (Const 9007199254740618%Z).
+Notation "'0x1ffffffffffe8a'" (* 9007199254740618 (0x1ffffffffffe8a) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~1~0~1~0).
 Notation "'0x1fffffffffffe3'" (* 9007199254740963 (0x1fffffffffffe3) *)
   := (Const 9007199254740963%Z).
 Notation "'0x1fffffffffffe3'" (* 9007199254740963 (0x1fffffffffffe3) *)