Add more constant notations

2 files changed, 200 insertions, 0 deletions

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 3edd4cb04..427282d35 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -69,6 +69,7 @@ nums = tuple(sorted(set(systematic_nums + [
     16777201,
     16777207,
     16777213,
+    33554399,
     33554413,
     33554417,
     33554427,
@@ -81,9 +82,11 @@ nums = tuple(sorted(set(systematic_nums + [
     67108861,
     67108862,
     134217690,
+    134217699,
     134217703,
     134217710,
     134217713,
+    134217719,
     134217726,
     268431360,
     268435441,
@@ -91,10 +94,12 @@ nums = tuple(sorted(set(systematic_nums + [
     268435454,
     536870893,
     536870906,
+    536870907,
     536870909,
     536870910,
     678152731,
     954437177,
+    1065418751,
     1073741821,
     1073741822,
     1332920885,
@@ -108,7 +113,10 @@ nums = tuple(sorted(set(systematic_nums + [
     3707621341,
     4008636143,
     4042322161,
+    4289200127,
+    4294963199,
     4294966319,
+    4294966531,
     4294967107,
     4294967179,
     4294967263,
@@ -167,6 +175,8 @@ nums = tuple(sorted(set(systematic_nums + [
     140737488355303,
     140737488355313,
     140737488355319,
+    194613558116351,
+    281453501874175,
     281470681743359,
     281474976645119,
     281474976710339,
@@ -202,7 +212,9 @@ nums = tuple(sorted(set(systematic_nums + [
     18014398509481975,
     18014398509481981,
     18014398509481982,
+    36028797018963937,
     36028797018963943,
+    36028797018963947,
     36028797018963949,
     72056494526300160,
     72057594037927819,
@@ -214,18 +226,24 @@ nums = tuple(sorted(set(systematic_nums + [
     144115188075855857,
     144115188075855863,
     144115188075855867,
+    144115188075855869,
+    144115188075855870,
     288230376151711717,
     288230376151711727,
     288230376151711741,
     576460752303423467,
     576460752303423469,
+    576460752303423471,
     1117984489315730401,
+    1152921504606846974,
     3353953467947191203,
     3816567739388183093,
+    4530058275181297663,
     4575938696385134591,
     5675921253449092805,
     9564978408590137875,
     9708812670373448219,
+    9963214713607832691,
     10248191152060862009,
     10330176681277348905,
     10365313336655843289,
@@ -237,17 +255,24 @@ nums = tuple(sorted(set(systematic_nums + [
     14933078535860113213,
     14978125529935106013,
     15580212934572586289,
+    17050145153302519317,
     17216961135462248175,
+    17256631552825064415,
     17361641481138401521,
+    18308539860144619519,
     18421974275759013887,
     18445336698825998335,
+    18446462598732840959,
     18446726481523507199,
     18446744065119617023,
     18446744069414583343,
     18446744069414584319,
     18446744069414584320,
     18446744069414584321,
+    18446744073709486079,
     18446744073709550851,
+    18446744073709551047,
+    18446744073709551135,
     18446744073709551195,
     18446744073709551299,
     18446744073709551427,
@@ -786,6 +811,8 @@ Notation "'0b1000000000000000000000000'" (* 16777216 (0x1000000) *)
   := (Const WO~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).
 Notation "'0b1000000000000000000000001'" (* 16777217 (0x1000001) *)
   := (Const WO~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~1).
+Notation "'0b1111111111111111111011111'" (* 33554399 (0x1ffffdf) *)
+  := (Const WO~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).
 Notation "'0b1111111111111111111101101'" (* 33554413 (0x1ffffed) *)
   := (Const WO~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~0~1).
 Notation "'0b1111111111111111111110001'" (* 33554417 (0x1fffff1) *)
@@ -822,12 +849,16 @@ Notation "'0b100000000000000000000000001'" (* 67108865 (0x4000001) *)
   := (Const WO~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~1).
 Notation "'0b111111111111111111111011010'" (* 134217690 (0x7ffffda) *)
   := (Const WO~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~1~0~1~0).
+Notation "'0b111111111111111111111100011'" (* 134217699 (0x7ffffe3) *)
+  := (Const WO~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~0~0~1~1).
 Notation "'0b111111111111111111111100111'" (* 134217703 (0x7ffffe7) *)
   := (Const WO~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~0~1~1~1).
 Notation "'0b111111111111111111111101110'" (* 134217710 (0x7ffffee) *)
   := (Const WO~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~1~1~0).
 Notation "'0b111111111111111111111110001'" (* 134217713 (0x7fffff1) *)
   := (Const WO~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~0~0~0~1).
+Notation "'0b111111111111111111111110111'" (* 134217719 (0x7fffff7) *)
+  := (Const WO~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~0~1~1~1).
 Notation "'0b111111111111111111111111110'" (* 134217726 (0x7fffffe) *)
   := (Const WO~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).
 Notation "'0b111111111111111111111111111'" (* 134217727 (0x7ffffff) *)
@@ -854,6 +885,8 @@ Notation "'0b11111111111111111111111101101'" (* 536870893 (0x1fffffed) *)
   := (Const WO~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~0~1~1~0~1).
 Notation "'0b11111111111111111111111111010'" (* 536870906 (0x1ffffffa) *)
   := (Const WO~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~0).
+Notation "'0b11111111111111111111111111011'" (* 536870907 (0x1ffffffb) *)
+  := (Const WO~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).
 Notation "'0b11111111111111111111111111101'" (* 536870909 (0x1ffffffd) *)
   := (Const WO~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~0~1).
 Notation "'0b11111111111111111111111111110'" (* 536870910 (0x1ffffffe) *)
@@ -868,6 +901,8 @@ Notation "'0b101000011010111100101000011011'" (* 678152731 (0x286bca1b) *)
   := (Const WO~0~0~1~0~1~0~0~0~0~1~1~0~1~0~1~1~1~1~0~0~1~0~1~0~0~0~0~1~1~0~1~1).
 Notation "'0b111000111000111000111000111001'" (* 954437177 (0x38e38e39) *)
   := (Const WO~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~1).
+Notation "'0b111111100000001111111111111111'" (* 1065418751 (0x3f80ffff) *)
+  := (Const WO~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~1~1~1~1~1~1~1).
 Notation "'0b111111111111111111111111111101'" (* 1073741821 (0x3ffffffd) *)
   := (Const WO~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~0~1).
 Notation "'0b111111111111111111111111111110'" (* 1073741822 (0x3ffffffe) *)
@@ -904,8 +939,14 @@ Notation "'0b11101110111011101110111011101111'" (* 4008636143 (0xeeeeeeef) *)
   := (Const WO~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~1).
 Notation "'0b11110000111100001111000011110001'" (* 4042322161 (0xf0f0f0f1) *)
   := (Const WO~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~1).
+Notation "'0b11111111101001111111111111111111'" (* 4289200127 (0xffa7ffff) *)
+  := (Const WO~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).
+Notation "'0b11111111111111111110111111111111'" (* 4294963199 (0xffffefff) *)
+  := (Const WO~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).
 Notation "'0b11111111111111111111110000101111'" (* 4294966319 (0xfffffc2f) *)
   := (Const WO~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).
+Notation "'0b11111111111111111111110100000011'" (* 4294966531 (0xfffffd03) *)
+  := (Const WO~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~0~0~1~1).
 Notation "'0b11111111111111111111111101000011'" (* 4294967107 (0xffffff43) *)
   := (Const WO~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).
 Notation "'0b11111111111111111111111110001011'" (* 4294967179 (0xffffff8b) *)
@@ -1118,6 +1159,10 @@ Notation "'0b100000000000000000000000000000000000000000000000'" (* 1407374883553
   := (Const WO~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~0~0~0~0~0~0~0~0).
 Notation "'0b100000000000000000000000000000000000000000000001'" (* 140737488355329 (0x800000000001) *)
   := (Const WO~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~0~0~0~0~0~0~0~1).
+Notation "'0b101100001111111111111111111111111111111111111111'" (* 194613558116351 (0xb0ffffffffff) *)
+  := (Const WO~0~0~0~0~0~0~0~0~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~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 "'0b111111111111101011111111111111111111111111111111'" (* 281453501874175 (0xfffaffffffff) *)
+  := (Const WO~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~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).
 Notation "'0b111111111111111011111111111111111111111111111111'" (* 281470681743359 (0xfffeffffffff) *)
   := (Const WO~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~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).
 Notation "'0b111111111111111111111111111111101111111111111111'" (* 281474976645119 (0xfffffffeffff) *)
@@ -1230,8 +1275,12 @@ Notation "'0b1000000000000000000000000000000000000000000000000000000'" (* 180143
   := (Const WO~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~0~0~0~0).
 Notation "'0b1000000000000000000000000000000000000000000000000000001'" (* 18014398509481985 (0x40000000000001) *)
   := (Const WO~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~0~0~0~1).
+Notation "'0b1111111111111111111111111111111111111111111111111100001'" (* 36028797018963937 (0x7fffffffffffe1) *)
+  := (Const WO~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~1~1~0~0~0~0~1).
 Notation "'0b1111111111111111111111111111111111111111111111111100111'" (* 36028797018963943 (0x7fffffffffffe7) *)
   := (Const WO~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~1~1~0~0~1~1~1).
+Notation "'0b1111111111111111111111111111111111111111111111111101011'" (* 36028797018963947 (0x7fffffffffffeb) *)
+  := (Const WO~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~1~1~0~1~0~1~1).
 Notation "'0b1111111111111111111111111111111111111111111111111101101'" (* 36028797018963949 (0x7fffffffffffed) *)
   := (Const WO~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~1~1~0~1~1~0~1).
 Notation "'0b1111111111111111111111111111111111111111111111111111111'" (* 36028797018963967 (0x7fffffffffffff) *)
@@ -1266,6 +1315,10 @@ Notation "'0b111111111111111111111111111111111111111111111111111110111'" (* 1441
   := (Const WO~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~1~1~1~1~1~0~1~1~1).
 Notation "'0b111111111111111111111111111111111111111111111111111111011'" (* 144115188075855867 (0x1fffffffffffffb) *)
   := (Const WO~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~1~1~1~1~1~1~0~1~1).
+Notation "'0b111111111111111111111111111111111111111111111111111111101'" (* 144115188075855869 (0x1fffffffffffffd) *)
+  := (Const WO~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~1~1~1~1~1~1~1~0~1).
+Notation "'0b111111111111111111111111111111111111111111111111111111110'" (* 144115188075855870 (0x1fffffffffffffe) *)
+  := (Const WO~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~1~1~1~1~1~1~1~1~0).
 Notation "'0b111111111111111111111111111111111111111111111111111111111'" (* 144115188075855871 (0x1ffffffffffffff) *)
   := (Const WO~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~1~1~1~1~1~1~1~1~1).
 Notation "'0b1000000000000000000000000000000000000000000000000000000000'" (* 144115188075855872 (0x200000000000000) *)
@@ -1288,6 +1341,8 @@ Notation "'0b11111111111111111111111111111111111111111111111111111101011'" (* 57
   := (Const WO~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~1~1~1~1~1~1~0~1~0~1~1).
 Notation "'0b11111111111111111111111111111111111111111111111111111101101'" (* 576460752303423469 (0x7ffffffffffffed) *)
   := (Const WO~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~1~1~1~1~1~1~0~1~1~0~1).
+Notation "'0b11111111111111111111111111111111111111111111111111111101111'" (* 576460752303423471 (0x7ffffffffffffef) *)
+  := (Const WO~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~1~1~1~1~1~1~0~1~1~1~1).
 Notation "'0b11111111111111111111111111111111111111111111111111111111111'" (* 576460752303423487 (0x7ffffffffffffff) *)
   := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b100000000000000000000000000000000000000000000000000000000000'" (* 576460752303423488 (0x800000000000000) *)
@@ -1296,6 +1351,8 @@ Notation "'0b100000000000000000000000000000000000000000000000000000000001'" (* 5
   := (Const WO~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~0~0~0~0~0~0~0~0~1).
 Notation "'0b111110000011111000001111100000111110000011111000001111100001'" (* 1117984489315730401 (0xf83e0f83e0f83e1) *)
   := (Const WO~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~1).
+Notation "'0b111111111111111111111111111111111111111111111111111111111110'" (* 1152921504606846974 (0xffffffffffffffe) *)
+  := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0b111111111111111111111111111111111111111111111111111111111111'" (* 1152921504606846975 (0xfffffffffffffff) *)
   := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b1000000000000000000000000000000000000000000000000000000000000'" (* 1152921504606846976 (0x1000000000000000) *)
@@ -1312,6 +1369,8 @@ Notation "'0b10111010001011101000101110100010111010001011101000101110100011'" (*
   := (Const WO~0~0~1~0~1~1~1~0~1~0~0~0~1~0~1~1~1~0~1~0~0~0~1~0~1~1~1~0~1~0~0~0~1~0~1~1~1~0~1~0~0~0~1~0~1~1~1~0~1~0~0~0~1~0~1~1~1~0~1~0~0~0~1~1).
 Notation "'0b11010011110111001011000010001101001111011100101100001000110101'" (* 3816567739388183093 (0x34f72c234f72c235) *)
   := (Const WO~0~0~1~1~0~1~0~0~1~1~1~1~0~1~1~1~0~0~1~0~1~1~0~0~0~0~1~0~0~0~1~1~0~1~0~0~1~1~1~1~0~1~1~1~0~0~1~0~1~1~0~0~0~0~1~0~0~0~1~1~0~1~0~1).
+Notation "'0b11111011011101111111111111111111111111111111111111111111111111'" (* 4530058275181297663 (0x3eddffffffffffff) *)
+  := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b11111110000000111111111111111111111111111111111111111111111111'" (* 4575938696385134591 (0x3f80ffffffffffff) *)
   := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0b11111111111111111111111111111111111111111111111111111111111111'" (* 4611686018427387903 (0x3fffffffffffffff) *)
@@ -1332,6 +1391,8 @@ Notation "'0b1000010010111101101000010010111101101000010010111101101000010011'"
   := (Const WO~1~0~0~0~0~1~0~0~1~0~1~1~1~1~0~1~1~0~1~0~0~0~0~1~0~0~1~0~1~1~1~1~0~1~1~0~1~0~0~0~0~1~0~0~1~0~1~1~1~1~0~1~1~0~1~0~0~0~0~1~0~0~1~1).
 Notation "'0b1000011010111100101000011010111100101000011010111100101000011011'" (* 9708812670373448219 (0x86bca1af286bca1bL) *)
   := (Const WO~1~0~0~0~0~1~1~0~1~0~1~1~1~1~0~0~1~0~1~0~0~0~0~1~1~0~1~0~1~1~1~1~0~0~1~0~1~0~0~0~0~1~1~0~1~0~1~1~1~1~0~0~1~0~1~0~0~0~0~1~1~0~1~1).
+Notation "'0b1000101001000100011100101111111010100001100010100100010001110011'" (* 9963214713607832691 (0x8a4472fea18a4473L) *)
+  := (Const WO~1~0~0~0~1~0~1~0~0~1~0~0~0~1~0~0~0~1~1~1~0~0~1~0~1~1~1~1~1~1~1~0~1~0~1~0~0~0~0~1~1~0~0~0~1~0~1~0~0~1~0~0~0~1~0~0~0~1~1~1~0~0~1~1).
 Notation "'0b1000111000111000111000111000111000111000111000111000111000111001'" (* 10248191152060862009 (0x8e38e38e38e38e39L) *)
   := (Const WO~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~1).
 Notation "'0b1000111101011100001010001111010111000010100011110101110000101001'" (* 10330176681277348905 (0x8f5c28f5c28f5c29L) *)
@@ -1354,14 +1415,22 @@ Notation "'0b1100111111011100111111011100111111011100111111011100111111011101'"
   := (Const WO~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~1).
 Notation "'0b1101100000111000000010010001110111010010001001010011010100110001'" (* 15580212934572586289 (0xd838091dd2253531L) *)
   := (Const WO~1~1~0~1~1~0~0~0~0~0~1~1~1~0~0~0~0~0~0~0~1~0~0~1~0~0~0~1~1~1~0~1~1~1~0~1~0~0~1~0~0~0~1~0~0~1~0~1~0~0~1~1~0~1~0~1~0~0~1~1~0~0~0~1).
+Notation "'0b1110110010011110010010001010111001101111011100011101111000010101'" (* 17050145153302519317 (0xec9e48ae6f71de15L) *)
+  := (Const WO~1~1~1~0~1~1~0~0~1~0~0~1~1~1~1~0~0~1~0~0~1~0~0~0~1~0~1~0~1~1~1~0~0~1~1~0~1~1~1~1~0~1~1~1~0~0~0~1~1~1~0~1~1~1~1~0~0~0~0~1~0~1~0~1).
 Notation "'0b1110111011101110111011101110111011101110111011101110111011101111'" (* 17216961135462248175 (0xeeeeeeeeeeeeeeefL) *)
   := (Const WO~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~1).
+Notation "'0b1110111101111011110111101111011110111101111011110111101111011111'" (* 17256631552825064415 (0xef7bdef7bdef7bdfL) *)
+  := (Const WO~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~1).
 Notation "'0b1111000011110000111100001111000011110000111100001111000011110001'" (* 17361641481138401521 (0xf0f0f0f0f0f0f0f1L) *)
   := (Const WO~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~1).
+Notation "'0b1111111000010100111111111111111111111111111111111111111111111111'" (* 18308539860144619519 (0xfe14ffffffffffffL) *)
+  := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b1111111110100111111111111111111111111111111111111111111111111111'" (* 18421974275759013887 (0xffa7ffffffffffffL) *)
   := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b1111111111111010111111111111111111111111111111111111111111111111'" (* 18445336698825998335 (0xfffaffffffffffffL) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~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~1~1~1~1).
+Notation "'0b1111111111111110111111111111111111111111111111111111111111111111'" (* 18446462598732840959 (0xfffeffffffffffffL) *)
+  := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b1111111111111111111011111111111111111111111111111111111111111111'" (* 18446726481523507199 (0xffffefffffffffffL) *)
   := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b1111111111111111111111111111110111111111111111111111111111111111'" (* 18446744065119617023 (0xfffffffdffffffffL) *)
@@ -1374,8 +1443,14 @@ Notation "'0b1111111111111111111111111111111100000000000000000000000000000000'"
   := (Const WO~1~1~1~1~1~1~1~1~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~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 "'0b1111111111111111111111111111111100000000000000000000000000000001'" (* 18446744069414584321 (0xffffffff00000001L) *)
   := (Const WO~1~1~1~1~1~1~1~1~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~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 "'0b1111111111111111111111111111111111111111111111101111111111111111'" (* 18446744073709486079 (0xfffffffffffeffffL) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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).
 Notation "'0b1111111111111111111111111111111111111111111111111111110100000011'" (* 18446744073709550851 (0xfffffffffffffd03L) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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~0~0~1~1).
+Notation "'0b1111111111111111111111111111111111111111111111111111110111000111'" (* 18446744073709551047 (0xfffffffffffffdc7L) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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).
+Notation "'0b1111111111111111111111111111111111111111111111111111111000011111'" (* 18446744073709551135 (0xfffffffffffffe1fL) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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).
 Notation "'0b1111111111111111111111111111111111111111111111111111111001011011'" (* 18446744073709551195 (0xfffffffffffffe5bL) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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~0~1~1).
 Notation "'0b1111111111111111111111111111111111111111111111111111111011000011'" (* 18446744073709551299 (0xfffffffffffffec3L) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 822fa7b7b..7c963f0e5 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -69,6 +69,7 @@ nums = tuple(sorted(set(systematic_nums + [
     16777201,
     16777207,
     16777213,
+    33554399,
     33554413,
     33554417,
     33554427,
@@ -81,9 +82,11 @@ nums = tuple(sorted(set(systematic_nums + [
     67108861,
     67108862,
     134217690,
+    134217699,
     134217703,
     134217710,
     134217713,
+    134217719,
     134217726,
     268431360,
     268435441,
@@ -91,10 +94,12 @@ nums = tuple(sorted(set(systematic_nums + [
     268435454,
     536870893,
     536870906,
+    536870907,
     536870909,
     536870910,
     678152731,
     954437177,
+    1065418751,
     1073741821,
     1073741822,
     1332920885,
@@ -108,7 +113,10 @@ nums = tuple(sorted(set(systematic_nums + [
     3707621341,
     4008636143,
     4042322161,
+    4289200127,
+    4294963199,
     4294966319,
+    4294966531,
     4294967107,
     4294967179,
     4294967263,
@@ -167,6 +175,8 @@ nums = tuple(sorted(set(systematic_nums + [
     140737488355303,
     140737488355313,
     140737488355319,
+    194613558116351,
+    281453501874175,
     281470681743359,
     281474976645119,
     281474976710339,
@@ -202,7 +212,9 @@ nums = tuple(sorted(set(systematic_nums + [
     18014398509481975,
     18014398509481981,
     18014398509481982,
+    36028797018963937,
     36028797018963943,
+    36028797018963947,
     36028797018963949,
     72056494526300160,
     72057594037927819,
@@ -214,18 +226,24 @@ nums = tuple(sorted(set(systematic_nums + [
     144115188075855857,
     144115188075855863,
     144115188075855867,
+    144115188075855869,
+    144115188075855870,
     288230376151711717,
     288230376151711727,
     288230376151711741,
     576460752303423467,
     576460752303423469,
+    576460752303423471,
     1117984489315730401,
+    1152921504606846974,
     3353953467947191203,
     3816567739388183093,
+    4530058275181297663,
     4575938696385134591,
     5675921253449092805,
     9564978408590137875,
     9708812670373448219,
+    9963214713607832691,
     10248191152060862009,
     10330176681277348905,
     10365313336655843289,
@@ -237,17 +255,24 @@ nums = tuple(sorted(set(systematic_nums + [
     14933078535860113213,
     14978125529935106013,
     15580212934572586289,
+    17050145153302519317,
     17216961135462248175,
+    17256631552825064415,
     17361641481138401521,
+    18308539860144619519,
     18421974275759013887,
     18445336698825998335,
+    18446462598732840959,
     18446726481523507199,
     18446744065119617023,
     18446744069414583343,
     18446744069414584319,
     18446744069414584320,
     18446744069414584321,
+    18446744073709486079,
     18446744073709550851,
+    18446744073709551047,
+    18446744073709551135,
     18446744073709551195,
     18446744073709551299,
     18446744073709551427,
@@ -1256,6 +1281,10 @@ Notation "'0x1000001'" (* 16777217 (0x1000001) *)
   := (Const 16777217%Z).
 Notation "'0x1000001'" (* 16777217 (0x1000001) *)
   := (Const WO~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~1).
+Notation "'0x1ffffdf'" (* 33554399 (0x1ffffdf) *)
+  := (Const 33554399%Z).
+Notation "'0x1ffffdf'" (* 33554399 (0x1ffffdf) *)
+  := (Const WO~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).
 Notation "'0x1ffffed'" (* 33554413 (0x1ffffed) *)
   := (Const 33554413%Z).
 Notation "'0x1ffffed'" (* 33554413 (0x1ffffed) *)
@@ -1328,6 +1357,10 @@ Notation "'0x7ffffda'" (* 134217690 (0x7ffffda) *)
   := (Const 134217690%Z).
 Notation "'0x7ffffda'" (* 134217690 (0x7ffffda) *)
   := (Const WO~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~1~0~1~0).
+Notation "'0x7ffffe3'" (* 134217699 (0x7ffffe3) *)
+  := (Const 134217699%Z).
+Notation "'0x7ffffe3'" (* 134217699 (0x7ffffe3) *)
+  := (Const WO~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~0~0~1~1).
 Notation "'0x7ffffe7'" (* 134217703 (0x7ffffe7) *)
   := (Const 134217703%Z).
 Notation "'0x7ffffe7'" (* 134217703 (0x7ffffe7) *)
@@ -1340,6 +1373,10 @@ Notation "'0x7fffff1'" (* 134217713 (0x7fffff1) *)
   := (Const 134217713%Z).
 Notation "'0x7fffff1'" (* 134217713 (0x7fffff1) *)
   := (Const WO~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~0~0~0~1).
+Notation "'0x7fffff7'" (* 134217719 (0x7fffff7) *)
+  := (Const 134217719%Z).
+Notation "'0x7fffff7'" (* 134217719 (0x7fffff7) *)
+  := (Const WO~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~0~1~1~1).
 Notation "'0x7fffffe'" (* 134217726 (0x7fffffe) *)
   := (Const 134217726%Z).
 Notation "'0x7fffffe'" (* 134217726 (0x7fffffe) *)
@@ -1392,6 +1429,10 @@ Notation "'0x1ffffffa'" (* 536870906 (0x1ffffffa) *)
   := (Const 536870906%Z).
 Notation "'0x1ffffffa'" (* 536870906 (0x1ffffffa) *)
   := (Const WO~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~0).
+Notation "'0x1ffffffb'" (* 536870907 (0x1ffffffb) *)
+  := (Const 536870907%Z).
+Notation "'0x1ffffffb'" (* 536870907 (0x1ffffffb) *)
+  := (Const WO~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).
 Notation "'0x1ffffffd'" (* 536870909 (0x1ffffffd) *)
   := (Const 536870909%Z).
 Notation "'0x1ffffffd'" (* 536870909 (0x1ffffffd) *)
@@ -1420,6 +1461,10 @@ Notation "'0x38e38e39'" (* 954437177 (0x38e38e39) *)
   := (Const 954437177%Z).
 Notation "'0x38e38e39'" (* 954437177 (0x38e38e39) *)
   := (Const WO~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~1).
+Notation "'0x3f80ffff'" (* 1065418751 (0x3f80ffff) *)
+  := (Const 1065418751%Z).
+Notation "'0x3f80ffff'" (* 1065418751 (0x3f80ffff) *)
+  := (Const WO~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~1~1~1~1~1~1~1).
 Notation "'0x3ffffffd'" (* 1073741821 (0x3ffffffd) *)
   := (Const 1073741821%Z).
 Notation "'0x3ffffffd'" (* 1073741821 (0x3ffffffd) *)
@@ -1492,10 +1537,22 @@ Notation "'0xf0f0f0f1'" (* 4042322161 (0xf0f0f0f1) *)
   := (Const 4042322161%Z).
 Notation "'0xf0f0f0f1'" (* 4042322161 (0xf0f0f0f1) *)
   := (Const WO~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~1).
+Notation "'0xffa7ffff'" (* 4289200127 (0xffa7ffff) *)
+  := (Const 4289200127%Z).
+Notation "'0xffa7ffff'" (* 4289200127 (0xffa7ffff) *)
+  := (Const WO~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).
+Notation "'0xffffefff'" (* 4294963199 (0xffffefff) *)
+  := (Const 4294963199%Z).
+Notation "'0xffffefff'" (* 4294963199 (0xffffefff) *)
+  := (Const WO~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).
 Notation "'0xfffffc2f'" (* 4294966319 (0xfffffc2f) *)
   := (Const 4294966319%Z).
 Notation "'0xfffffc2f'" (* 4294966319 (0xfffffc2f) *)
   := (Const WO~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).
+Notation "'0xfffffd03'" (* 4294966531 (0xfffffd03) *)
+  := (Const 4294966531%Z).
+Notation "'0xfffffd03'" (* 4294966531 (0xfffffd03) *)
+  := (Const WO~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~0~0~1~1).
 Notation "'0xffffff43'" (* 4294967107 (0xffffff43) *)
   := (Const 4294967107%Z).
 Notation "'0xffffff43'" (* 4294967107 (0xffffff43) *)
@@ -1920,6 +1977,14 @@ Notation "'0x800000000001'" (* 140737488355329 (0x800000000001) *)
   := (Const 140737488355329%Z).
 Notation "'0x800000000001'" (* 140737488355329 (0x800000000001) *)
   := (Const WO~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~0~0~0~0~0~0~0~1).
+Notation "'0xb0ffffffffff'" (* 194613558116351 (0xb0ffffffffff) *)
+  := (Const 194613558116351%Z).
+Notation "'0xb0ffffffffff'" (* 194613558116351 (0xb0ffffffffff) *)
+  := (Const WO~0~0~0~0~0~0~0~0~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~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 "'0xfffaffffffff'" (* 281453501874175 (0xfffaffffffff) *)
+  := (Const 281453501874175%Z).
+Notation "'0xfffaffffffff'" (* 281453501874175 (0xfffaffffffff) *)
+  := (Const WO~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~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).
 Notation "'0xfffeffffffff'" (* 281470681743359 (0xfffeffffffff) *)
   := (Const 281470681743359%Z).
 Notation "'0xfffeffffffff'" (* 281470681743359 (0xfffeffffffff) *)
@@ -2144,10 +2209,18 @@ Notation "'0x40000000000001'" (* 18014398509481985 (0x40000000000001) *)
   := (Const 18014398509481985%Z).
 Notation "'0x40000000000001'" (* 18014398509481985 (0x40000000000001) *)
   := (Const WO~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~0~0~0~1).
+Notation "'0x7fffffffffffe1'" (* 36028797018963937 (0x7fffffffffffe1) *)
+  := (Const 36028797018963937%Z).
+Notation "'0x7fffffffffffe1'" (* 36028797018963937 (0x7fffffffffffe1) *)
+  := (Const WO~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~1~1~0~0~0~0~1).
 Notation "'0x7fffffffffffe7'" (* 36028797018963943 (0x7fffffffffffe7) *)
   := (Const 36028797018963943%Z).
 Notation "'0x7fffffffffffe7'" (* 36028797018963943 (0x7fffffffffffe7) *)
   := (Const WO~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~1~1~0~0~1~1~1).
+Notation "'0x7fffffffffffeb'" (* 36028797018963947 (0x7fffffffffffeb) *)
+  := (Const 36028797018963947%Z).
+Notation "'0x7fffffffffffeb'" (* 36028797018963947 (0x7fffffffffffeb) *)
+  := (Const WO~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~1~1~0~1~0~1~1).
 Notation "'0x7fffffffffffed'" (* 36028797018963949 (0x7fffffffffffed) *)
   := (Const 36028797018963949%Z).
 Notation "'0x7fffffffffffed'" (* 36028797018963949 (0x7fffffffffffed) *)
@@ -2216,6 +2289,14 @@ Notation "'0x1fffffffffffffb'" (* 144115188075855867 (0x1fffffffffffffb) *)
   := (Const 144115188075855867%Z).
 Notation "'0x1fffffffffffffb'" (* 144115188075855867 (0x1fffffffffffffb) *)
   := (Const WO~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~1~1~1~1~1~1~0~1~1).
+Notation "'0x1fffffffffffffd'" (* 144115188075855869 (0x1fffffffffffffd) *)
+  := (Const 144115188075855869%Z).
+Notation "'0x1fffffffffffffd'" (* 144115188075855869 (0x1fffffffffffffd) *)
+  := (Const WO~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~1~1~1~1~1~1~1~0~1).
+Notation "'0x1fffffffffffffe'" (* 144115188075855870 (0x1fffffffffffffe) *)
+  := (Const 144115188075855870%Z).
+Notation "'0x1fffffffffffffe'" (* 144115188075855870 (0x1fffffffffffffe) *)
+  := (Const WO~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~1~1~1~1~1~1~1~1~0).
 Notation "'0x1ffffffffffffff'" (* 144115188075855871 (0x1ffffffffffffff) *)
   := (Const 144115188075855871%Z).
 Notation "'0x1ffffffffffffff'" (* 144115188075855871 (0x1ffffffffffffff) *)
@@ -2260,6 +2341,10 @@ Notation "'0x7ffffffffffffed'" (* 576460752303423469 (0x7ffffffffffffed) *)
   := (Const 576460752303423469%Z).
 Notation "'0x7ffffffffffffed'" (* 576460752303423469 (0x7ffffffffffffed) *)
   := (Const WO~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~1~1~1~1~1~1~0~1~1~0~1).
+Notation "'0x7ffffffffffffef'" (* 576460752303423471 (0x7ffffffffffffef) *)
+  := (Const 576460752303423471%Z).
+Notation "'0x7ffffffffffffef'" (* 576460752303423471 (0x7ffffffffffffef) *)
+  := (Const WO~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~1~1~1~1~1~1~0~1~1~1~1).
 Notation "'0x7ffffffffffffff'" (* 576460752303423487 (0x7ffffffffffffff) *)
   := (Const 576460752303423487%Z).
 Notation "'0x7ffffffffffffff'" (* 576460752303423487 (0x7ffffffffffffff) *)
@@ -2276,6 +2361,10 @@ Notation "'0xf83e0f83e0f83e1'" (* 1117984489315730401 (0xf83e0f83e0f83e1) *)
   := (Const 1117984489315730401%Z).
 Notation "'0xf83e0f83e0f83e1'" (* 1117984489315730401 (0xf83e0f83e0f83e1) *)
   := (Const WO~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~1).
+Notation "'0xffffffffffffffe'" (* 1152921504606846974 (0xffffffffffffffe) *)
+  := (Const 1152921504606846974%Z).
+Notation "'0xffffffffffffffe'" (* 1152921504606846974 (0xffffffffffffffe) *)
+  := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0xfffffffffffffff'" (* 1152921504606846975 (0xfffffffffffffff) *)
   := (Const 1152921504606846975%Z).
 Notation "'0xfffffffffffffff'" (* 1152921504606846975 (0xfffffffffffffff) *)
@@ -2308,6 +2397,10 @@ Notation "'0x34f72c234f72c235'" (* 3816567739388183093 (0x34f72c234f72c235) *)
   := (Const 3816567739388183093%Z).
 Notation "'0x34f72c234f72c235'" (* 3816567739388183093 (0x34f72c234f72c235) *)
   := (Const WO~0~0~1~1~0~1~0~0~1~1~1~1~0~1~1~1~0~0~1~0~1~1~0~0~0~0~1~0~0~0~1~1~0~1~0~0~1~1~1~1~0~1~1~1~0~0~1~0~1~1~0~0~0~0~1~0~0~0~1~1~0~1~0~1).
+Notation "'0x3eddffffffffffff'" (* 4530058275181297663 (0x3eddffffffffffff) *)
+  := (Const 4530058275181297663%Z).
+Notation "'0x3eddffffffffffff'" (* 4530058275181297663 (0x3eddffffffffffff) *)
+  := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0x3f80ffffffffffff'" (* 4575938696385134591 (0x3f80ffffffffffff) *)
   := (Const 4575938696385134591%Z).
 Notation "'0x3f80ffffffffffff'" (* 4575938696385134591 (0x3f80ffffffffffff) *)
@@ -2348,6 +2441,10 @@ Notation "'0x86bca1af286bca1bL'" (* 9708812670373448219 (0x86bca1af286bca1bL) *)
   := (Const 9708812670373448219%Z).
 Notation "'0x86bca1af286bca1bL'" (* 9708812670373448219 (0x86bca1af286bca1bL) *)
   := (Const WO~1~0~0~0~0~1~1~0~1~0~1~1~1~1~0~0~1~0~1~0~0~0~0~1~1~0~1~0~1~1~1~1~0~0~1~0~1~0~0~0~0~1~1~0~1~0~1~1~1~1~0~0~1~0~1~0~0~0~0~1~1~0~1~1).
+Notation "'0x8a4472fea18a4473L'" (* 9963214713607832691 (0x8a4472fea18a4473L) *)
+  := (Const 9963214713607832691%Z).
+Notation "'0x8a4472fea18a4473L'" (* 9963214713607832691 (0x8a4472fea18a4473L) *)
+  := (Const WO~1~0~0~0~1~0~1~0~0~1~0~0~0~1~0~0~0~1~1~1~0~0~1~0~1~1~1~1~1~1~1~0~1~0~1~0~0~0~0~1~1~0~0~0~1~0~1~0~0~1~0~0~0~1~0~0~0~1~1~1~0~0~1~1).
 Notation "'0x8e38e38e38e38e39L'" (* 10248191152060862009 (0x8e38e38e38e38e39L) *)
   := (Const 10248191152060862009%Z).
 Notation "'0x8e38e38e38e38e39L'" (* 10248191152060862009 (0x8e38e38e38e38e39L) *)
@@ -2392,14 +2489,26 @@ Notation "'0xd838091dd2253531L'" (* 15580212934572586289 (0xd838091dd2253531L) *
   := (Const 15580212934572586289%Z).
 Notation "'0xd838091dd2253531L'" (* 15580212934572586289 (0xd838091dd2253531L) *)
   := (Const WO~1~1~0~1~1~0~0~0~0~0~1~1~1~0~0~0~0~0~0~0~1~0~0~1~0~0~0~1~1~1~0~1~1~1~0~1~0~0~1~0~0~0~1~0~0~1~0~1~0~0~1~1~0~1~0~1~0~0~1~1~0~0~0~1).
+Notation "'0xec9e48ae6f71de15L'" (* 17050145153302519317 (0xec9e48ae6f71de15L) *)
+  := (Const 17050145153302519317%Z).
+Notation "'0xec9e48ae6f71de15L'" (* 17050145153302519317 (0xec9e48ae6f71de15L) *)
+  := (Const WO~1~1~1~0~1~1~0~0~1~0~0~1~1~1~1~0~0~1~0~0~1~0~0~0~1~0~1~0~1~1~1~0~0~1~1~0~1~1~1~1~0~1~1~1~0~0~0~1~1~1~0~1~1~1~1~0~0~0~0~1~0~1~0~1).
 Notation "'0xeeeeeeeeeeeeeeefL'" (* 17216961135462248175 (0xeeeeeeeeeeeeeeefL) *)
   := (Const 17216961135462248175%Z).
 Notation "'0xeeeeeeeeeeeeeeefL'" (* 17216961135462248175 (0xeeeeeeeeeeeeeeefL) *)
   := (Const WO~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~1).
+Notation "'0xef7bdef7bdef7bdfL'" (* 17256631552825064415 (0xef7bdef7bdef7bdfL) *)
+  := (Const 17256631552825064415%Z).
+Notation "'0xef7bdef7bdef7bdfL'" (* 17256631552825064415 (0xef7bdef7bdef7bdfL) *)
+  := (Const WO~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~1).
 Notation "'0xf0f0f0f0f0f0f0f1L'" (* 17361641481138401521 (0xf0f0f0f0f0f0f0f1L) *)
   := (Const 17361641481138401521%Z).
 Notation "'0xf0f0f0f0f0f0f0f1L'" (* 17361641481138401521 (0xf0f0f0f0f0f0f0f1L) *)
   := (Const WO~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~1).
+Notation "'0xfe14ffffffffffffL'" (* 18308539860144619519 (0xfe14ffffffffffffL) *)
+  := (Const 18308539860144619519%Z).
+Notation "'0xfe14ffffffffffffL'" (* 18308539860144619519 (0xfe14ffffffffffffL) *)
+  := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0xffa7ffffffffffffL'" (* 18421974275759013887 (0xffa7ffffffffffffL) *)
   := (Const 18421974275759013887%Z).
 Notation "'0xffa7ffffffffffffL'" (* 18421974275759013887 (0xffa7ffffffffffffL) *)
@@ -2408,6 +2517,10 @@ Notation "'0xfffaffffffffffffL'" (* 18445336698825998335 (0xfffaffffffffffffL) *
   := (Const 18445336698825998335%Z).
 Notation "'0xfffaffffffffffffL'" (* 18445336698825998335 (0xfffaffffffffffffL) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~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~1~1~1~1).
+Notation "'0xfffeffffffffffffL'" (* 18446462598732840959 (0xfffeffffffffffffL) *)
+  := (Const 18446462598732840959%Z).
+Notation "'0xfffeffffffffffffL'" (* 18446462598732840959 (0xfffeffffffffffffL) *)
+  := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0xffffefffffffffffL'" (* 18446726481523507199 (0xffffefffffffffffL) *)
   := (Const 18446726481523507199%Z).
 Notation "'0xffffefffffffffffL'" (* 18446726481523507199 (0xffffefffffffffffL) *)
@@ -2432,10 +2545,22 @@ Notation "'0xffffffff00000001L'" (* 18446744069414584321 (0xffffffff00000001L) *
   := (Const 18446744069414584321%Z).
 Notation "'0xffffffff00000001L'" (* 18446744069414584321 (0xffffffff00000001L) *)
   := (Const WO~1~1~1~1~1~1~1~1~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~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 "'0xfffffffffffeffffL'" (* 18446744073709486079 (0xfffffffffffeffffL) *)
+  := (Const 18446744073709486079%Z).
+Notation "'0xfffffffffffeffffL'" (* 18446744073709486079 (0xfffffffffffeffffL) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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).
 Notation "'0xfffffffffffffd03L'" (* 18446744073709550851 (0xfffffffffffffd03L) *)
   := (Const 18446744073709550851%Z).
 Notation "'0xfffffffffffffd03L'" (* 18446744073709550851 (0xfffffffffffffd03L) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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~0~0~1~1).
+Notation "'0xfffffffffffffdc7L'" (* 18446744073709551047 (0xfffffffffffffdc7L) *)
+  := (Const 18446744073709551047%Z).
+Notation "'0xfffffffffffffdc7L'" (* 18446744073709551047 (0xfffffffffffffdc7L) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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).
+Notation "'0xfffffffffffffe1fL'" (* 18446744073709551135 (0xfffffffffffffe1fL) *)
+  := (Const 18446744073709551135%Z).
+Notation "'0xfffffffffffffe1fL'" (* 18446744073709551135 (0xfffffffffffffe1fL) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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).
 Notation "'0xfffffffffffffe5bL'" (* 18446744073709551195 (0xfffffffffffffe5bL) *)
   := (Const 18446744073709551195%Z).
 Notation "'0xfffffffffffffe5bL'" (* 18446744073709551195 (0xfffffffffffffe5bL) *)