aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-11-12 22:17:37 -0500
committerGravatar Jason Gross <jgross@mit.edu>2017-11-12 22:17:37 -0500
commit8fd656355fddcc017af3064db74b1ecf3eabdf2c (patch)
treea36cc7c3ee752402947c5ee87428873e543d8ff9 /src
parenta3a91aa9f0dcf3c94e546aec1698390c9a0b7638 (diff)
Add more constant notations
Diffstat (limited to 'src')
-rw-r--r--src/Compilers/Z/BinaryNotationConstants.v138
-rw-r--r--src/Compilers/Z/HexNotationConstants.v230
2 files changed, 368 insertions, 0 deletions
diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 5e33f403e..ae48d7481 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -18,6 +18,7 @@ nums = tuple(sorted(set(systematic_nums + [
187,
189,
317,
+ 421,
481,
569,
765,
@@ -141,7 +142,9 @@ nums = tuple(sorted(set(systematic_nums + [
33554427,
33554429,
33554430,
+ 67107887,
67108798,
+ 67108799,
67108826,
67108833,
67108839,
@@ -154,6 +157,8 @@ nums = tuple(sorted(set(systematic_nums + [
67108859,
67108861,
67108862,
+ 134215774,
+ 134217598,
134217666,
134217678,
134217690,
@@ -177,14 +182,17 @@ nums = tuple(sorted(set(systematic_nums + [
268435441,
268435443,
268435445,
+ 268435447,
268435451,
268435452,
268435453,
268435454,
+ 536869935,
536870882,
536870886,
536870890,
536870893,
+ 536870894,
536870902,
536870906,
536870907,
@@ -196,6 +204,7 @@ nums = tuple(sorted(set(systematic_nums + [
1054736383,
1065418751,
1073709055,
+ 1073739870,
1073741786,
1073741814,
1073741818,
@@ -249,6 +258,7 @@ nums = tuple(sorted(set(systematic_nums + [
4294967291,
4294967293,
4294967294,
+ 4294968273,
8589934559,
8589934567,
8589934575,
@@ -345,16 +355,20 @@ nums = tuple(sorted(set(systematic_nums + [
70368744177637,
70368744177647,
70368744177651,
+ 70368744177655,
70368744177658,
70368744177659,
+ 70368744177660,
70368744177661,
70368744177662,
140737471578110,
+ 140737479966719,
140737488355274,
140737488355294,
140737488355301,
140737488355302,
140737488355303,
+ 140737488355310,
140737488355313,
140737488355318,
140737488355319,
@@ -362,10 +376,15 @@ nums = tuple(sorted(set(systematic_nums + [
194613558116351,
281453501874175,
281470681743359,
+ 281474959933438,
281474976645119,
+ 281474976710235,
281474976710339,
+ 281474976710469,
+ 281474976710551,
281474976710602,
281474976710606,
+ 281474976710625,
281474976710626,
281474976710631,
281474976710637,
@@ -378,18 +397,26 @@ nums = tuple(sorted(set(systematic_nums + [
389227116232702,
562907003748350,
562949953290238,
+ 562949953420470,
562949953420678,
+ 562949953420938,
+ 562949953421102,
+ 562949953421250,
562949953421262,
562949953421274,
+ 562949953421278,
562949953421279,
562949953421290,
+ 562949953421291,
562949953421293,
562949953421294,
562949953421297,
562949953421303,
+ 562949953421306,
562949953421310,
1125899873288191,
1125899906842558,
+ 1125899906842582,
1125899906842586,
1125899906842593,
1125899906842594,
@@ -412,6 +439,7 @@ nums = tuple(sorted(set(systematic_nums + [
2251799813685238,
2251799813685239,
2251799813685242,
+ 2251799813685245,
2251799813685246,
2920302883373054,
4423885034356734,
@@ -426,8 +454,10 @@ nums = tuple(sorted(set(systematic_nums + [
4503599627370434,
4503599627370458,
4503599627370462,
+ 4503599627370475,
4503599627370478,
4503599627370479,
+ 4503599627370490,
4503599627370491,
4503599627370494,
9007190664804446,
@@ -436,16 +466,24 @@ nums = tuple(sorted(set(systematic_nums + [
9007199254740030,
9007199254740614,
9007199254740618,
+ 9007199254740950,
+ 9007199254740958,
9007199254740963,
+ 9007199254740967,
9007199254740977,
9007199254740982,
9007199254740988,
9007199254740990,
18014398509481926,
+ 18014398509481934,
18014398509481954,
18014398509481975,
18014398509481981,
18014398509481982,
+ 36028797018963547,
+ 36028797018963651,
+ 36028797018963781,
+ 36028797018963863,
36028797018963937,
36028797018963943,
36028797018963947,
@@ -455,16 +493,22 @@ nums = tuple(sorted(set(systematic_nums + [
36028797018963964,
36028797018963966,
72056494526300160,
+ 72057594037927094,
+ 72057594037927302,
+ 72057594037927562,
+ 72057594037927726,
72057594037927819,
72057594037927874,
72057594037927886,
72057594037927894,
72057594037927898,
+ 72057594037927915,
72057594037927919,
72057594037927931,
72057594037927933,
72057594037927934,
144115188075855638,
+ 144115188075855830,
144115188075855838,
144115188075855853,
144115188075855857,
@@ -476,6 +520,7 @@ nums = tuple(sorted(set(systematic_nums + [
144115188075855869,
144115188075855870,
288230376151711706,
+ 288230376151711713,
288230376151711714,
288230376151711717,
288230376151711726,
@@ -485,6 +530,7 @@ nums = tuple(sorted(set(systematic_nums + [
288230376151711740,
288230376151711741,
288230376151711742,
+ 576460752303423426,
576460752303423434,
576460752303423454,
576460752303423467,
@@ -879,6 +925,8 @@ Notation "'0b100000001'" (* 257 (0x101) *)
:= (Const WO~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~1).
Notation "'0b100111101'" (* 317 (0x13d) *)
:= (Const WO~0~0~0~0~0~0~0~1~0~0~1~1~1~1~0~1).
+Notation "'0b110100101'" (* 421 (0x1a5) *)
+ := (Const WO~0~0~0~0~0~0~0~1~1~0~1~0~0~1~0~1).
Notation "'0b111100001'" (* 481 (0x1e1) *)
:= (Const WO~0~0~0~0~0~0~0~1~1~1~1~0~0~0~0~1).
Notation "'0b111111111'" (* 511 (0x1ff) *)
@@ -1227,8 +1275,12 @@ Notation "'0b10000000000000000000000000'" (* 33554432 (0x2000000) *)
:= (Const WO~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).
Notation "'0b10000000000000000000000001'" (* 33554433 (0x2000001) *)
:= (Const WO~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~1).
+Notation "'0b11111111111111110000101111'" (* 67107887 (0x3fffc2f) *)
+ := (Const WO~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~0~1~0~1~1~1~1).
Notation "'0b11111111111111111110111110'" (* 67108798 (0x3ffffbe) *)
:= (Const WO~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~0).
+Notation "'0b11111111111111111110111111'" (* 67108799 (0x3ffffbf) *)
+ := (Const WO~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).
Notation "'0b11111111111111111111011010'" (* 67108826 (0x3ffffda) *)
:= (Const WO~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~0).
Notation "'0b11111111111111111111100001'" (* 67108833 (0x3ffffe1) *)
@@ -1259,6 +1311,10 @@ Notation "'0b100000000000000000000000000'" (* 67108864 (0x4000000) *)
:= (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~0).
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 "'0b111111111111111100001011110'" (* 134215774 (0x7fff85e) *)
+ := (Const WO~0~0~0~0~0~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 "'0b111111111111111111101111110'" (* 134217598 (0x7ffff7e) *)
+ := (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~0~1~1~1~1~1~1~0).
Notation "'0b111111111111111111111000010'" (* 134217666 (0x7ffffc2) *)
:= (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~0~0~0~1~0).
Notation "'0b111111111111111111111001110'" (* 134217678 (0x7ffffce) *)
@@ -1311,6 +1367,8 @@ Notation "'0b1111111111111111111111110011'" (* 268435443 (0xffffff3) *)
:= (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~0~0~1~1).
Notation "'0b1111111111111111111111110101'" (* 268435445 (0xffffff5) *)
:= (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~0~1~0~1).
+Notation "'0b1111111111111111111111110111'" (* 268435447 (0xffffff7) *)
+ := (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~0~1~1~1).
Notation "'0b1111111111111111111111111011'" (* 268435451 (0xffffffb) *)
:= (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~0~1~1).
Notation "'0b1111111111111111111111111100'" (* 268435452 (0xffffffc) *)
@@ -1325,6 +1383,8 @@ Notation "'0b10000000000000000000000000000'" (* 268435456 (0x10000000) *)
:= (Const WO~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).
Notation "'0b10000000000000000000000000001'" (* 268435457 (0x10000001) *)
:= (Const WO~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~1).
+Notation "'0b11111111111111111110000101111'" (* 536869935 (0x1ffffc2f) *)
+ := (Const WO~0~0~0~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 "'0b11111111111111111111111100010'" (* 536870882 (0x1fffffe2) *)
:= (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~0~0~1~0).
Notation "'0b11111111111111111111111100110'" (* 536870886 (0x1fffffe6) *)
@@ -1333,6 +1393,8 @@ Notation "'0b11111111111111111111111101010'" (* 536870890 (0x1fffffea) *)
:= (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~0~1~0).
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 "'0b11111111111111111111111101110'" (* 536870894 (0x1fffffee) *)
+ := (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~1~0).
Notation "'0b11111111111111111111111110110'" (* 536870902 (0x1ffffff6) *)
:= (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~0~1~1~0).
Notation "'0b11111111111111111111111111010'" (* 536870906 (0x1ffffffa) *)
@@ -1361,6 +1423,8 @@ 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 "'0b111111111111110111111111111111'" (* 1073709055 (0x3fff7fff) *)
:= (Const WO~0~0~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).
+Notation "'0b111111111111111111100001011110'" (* 1073739870 (0x3ffff85e) *)
+ := (Const WO~0~0~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 "'0b111111111111111111111111011010'" (* 1073741786 (0x3fffffda) *)
:= (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~0~1~1~0~1~0).
Notation "'0b111111111111111111111111110110'" (* 1073741814 (0x3ffffff6) *)
@@ -1483,6 +1547,8 @@ Notation "'0b100000000000000000000000000000000'" (* 4294967296 (0x100000000) *)
:= (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~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).
Notation "'0b100000000000000000000000000000001'" (* 4294967297 (0x100000001) *)
:= (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~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~1).
+Notation "'0b100000000000000000000001111010001'" (* 4294968273 (0x1000003d1) *)
+ := (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~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~1~1~1~0~1~0~0~0~1).
Notation "'0b111111111111111111111111111011111'" (* 8589934559 (0x1ffffffdf) *)
:= (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~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~0~1~1~1~1~1).
Notation "'0b111111111111111111111111111100111'" (* 8589934567 (0x1ffffffe7) *)
@@ -1753,10 +1819,14 @@ Notation "'0b1111111111111111111111111111111111111111101111'" (* 70368744177647
:= (Const WO~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~1~1~1~1~1~1~1~0~1~1~1~1).
Notation "'0b1111111111111111111111111111111111111111110011'" (* 70368744177651 (0x3ffffffffff3) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~0~0~1~1).
+Notation "'0b1111111111111111111111111111111111111111110111'" (* 70368744177655 (0x3ffffffffff7) *)
+ := (Const WO~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~1~1~1~1~1~1~1~1~0~1~1~1).
Notation "'0b1111111111111111111111111111111111111111111010'" (* 70368744177658 (0x3ffffffffffa) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~1~0~1~0).
Notation "'0b1111111111111111111111111111111111111111111011'" (* 70368744177659 (0x3ffffffffffb) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~1~0~1~1).
+Notation "'0b1111111111111111111111111111111111111111111100'" (* 70368744177660 (0x3ffffffffffc) *)
+ := (Const WO~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~1~1~1~1~1~1~1~1~1~1~0~0).
Notation "'0b1111111111111111111111111111111111111111111101'" (* 70368744177661 (0x3ffffffffffd) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~1~1~0~1).
Notation "'0b1111111111111111111111111111111111111111111110'" (* 70368744177662 (0x3ffffffffffe) *)
@@ -1769,6 +1839,8 @@ Notation "'0b10000000000000000000000000000000000000000000001'" (* 70368744177665
:= (Const WO~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~0~0~0~0~0~0~1).
Notation "'0b11111111111111111111110111111111111111111111110'" (* 140737471578110 (0x7ffffefffffe) *)
:= (Const WO~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~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).
+Notation "'0b11111111111111111111111011111111111111111111111'" (* 140737479966719 (0x7fffff7fffff) *)
+ := (Const WO~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~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
Notation "'0b11111111111111111111111111111111111111111001010'" (* 140737488355274 (0x7fffffffffca) *)
:= (Const WO~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~1~1~1~1~1~1~1~0~0~1~0~1~0).
Notation "'0b11111111111111111111111111111111111111111011110'" (* 140737488355294 (0x7fffffffffde) *)
@@ -1779,6 +1851,8 @@ Notation "'0b11111111111111111111111111111111111111111100110'" (* 14073748835530
:= (Const WO~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~1~1~1~1~1~1~1~1~0~0~1~1~0).
Notation "'0b11111111111111111111111111111111111111111100111'" (* 140737488355303 (0x7fffffffffe7) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~0~0~1~1~1).
+Notation "'0b11111111111111111111111111111111111111111101110'" (* 140737488355310 (0x7fffffffffee) *)
+ := (Const WO~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~1~1~1~1~1~1~1~1~0~1~1~1~0).
Notation "'0b11111111111111111111111111111111111111111110001'" (* 140737488355313 (0x7ffffffffff1) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~1~0~0~0~1).
Notation "'0b11111111111111111111111111111111111111111110110'" (* 140737488355318 (0x7ffffffffff6) *)
@@ -1799,14 +1873,24 @@ Notation "'0b111111111111101011111111111111111111111111111111'" (* 2814535018741
:= (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 "'0b111111111111111111111110111111111111111111111110'" (* 281474959933438 (0xfffffefffffe) *)
+ := (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~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~0).
Notation "'0b111111111111111111111111111111101111111111111111'" (* 281474976645119 (0xfffffffeffff) *)
:= (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~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 "'0b111111111111111111111111111111111111111001011011'" (* 281474976710235 (0xfffffffffe5b) *)
+ := (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~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 "'0b111111111111111111111111111111111111111011000011'" (* 281474976710339 (0xfffffffffec3) *)
:= (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~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~0~0~0~1~1).
+Notation "'0b111111111111111111111111111111111111111101000101'" (* 281474976710469 (0xffffffffff45) *)
+ := (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~1~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).
+Notation "'0b111111111111111111111111111111111111111110010111'" (* 281474976710551 (0xffffffffff97) *)
+ := (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~1~1~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).
Notation "'0b111111111111111111111111111111111111111111001010'" (* 281474976710602 (0xffffffffffca) *)
:= (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~1~1~1~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~0).
Notation "'0b111111111111111111111111111111111111111111001110'" (* 281474976710606 (0xffffffffffce) *)
:= (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~1~1~1~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~0).
+Notation "'0b111111111111111111111111111111111111111111100001'" (* 281474976710625 (0xffffffffffe1) *)
+ := (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~1~1~1~1~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 "'0b111111111111111111111111111111111111111111100010'" (* 281474976710626 (0xffffffffffe2) *)
:= (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~1~1~1~1~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~0).
Notation "'0b111111111111111111111111111111111111111111100111'" (* 281474976710631 (0xffffffffffe7) *)
@@ -1837,16 +1921,28 @@ Notation "'0b1111111111111010111111111111111111111111111111110'" (* 562907003748
:= (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~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).
Notation "'0b1111111111111111111111111111111011111111111111110'" (* 562949953290238 (0x1fffffffdfffe) *)
:= (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~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~0).
+Notation "'0b1111111111111111111111111111111111111110010110110'" (* 562949953420470 (0x1fffffffffcb6) *)
+ := (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~1~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~0).
Notation "'0b1111111111111111111111111111111111111110110000110'" (* 562949953420678 (0x1fffffffffd86) *)
:= (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~1~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~0~0~0~1~1~0).
+Notation "'0b1111111111111111111111111111111111111111010001010'" (* 562949953420938 (0x1fffffffffe8a) *)
+ := (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~1~1~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 "'0b1111111111111111111111111111111111111111100101110'" (* 562949953421102 (0x1ffffffffff2e) *)
+ := (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~1~1~1~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 "'0b1111111111111111111111111111111111111111111000010'" (* 562949953421250 (0x1ffffffffffc2) *)
+ := (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~1~1~1~1~1~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~0).
Notation "'0b1111111111111111111111111111111111111111111001110'" (* 562949953421262 (0x1ffffffffffce) *)
:= (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~1~1~1~1~1~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~0).
Notation "'0b1111111111111111111111111111111111111111111011010'" (* 562949953421274 (0x1ffffffffffda) *)
:= (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~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111011110'" (* 562949953421278 (0x1ffffffffffde) *)
+ := (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~1~1~1~1~1~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~0).
Notation "'0b1111111111111111111111111111111111111111111011111'" (* 562949953421279 (0x1ffffffffffdf) *)
:= (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~1~1~1~1~1~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).
Notation "'0b1111111111111111111111111111111111111111111101010'" (* 562949953421290 (0x1ffffffffffea) *)
:= (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~1~1~1~1~1~1~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~0).
+Notation "'0b1111111111111111111111111111111111111111111101011'" (* 562949953421291 (0x1ffffffffffeb) *)
+ := (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~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111101101'" (* 562949953421293 (0x1ffffffffffed) *)
:= (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~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111101110'" (* 562949953421294 (0x1ffffffffffee) *)
@@ -1855,6 +1951,8 @@ Notation "'0b1111111111111111111111111111111111111111111110001'" (* 562949953421
:= (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~1~1~1~1~1~1~1~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).
Notation "'0b1111111111111111111111111111111111111111111110111'" (* 562949953421303 (0x1fffffffffff7) *)
:= (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~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111010'" (* 562949953421306 (0x1fffffffffffa) *)
+ := (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~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111110'" (* 562949953421310 (0x1fffffffffffe) *)
:= (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~1~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111'" (* 562949953421311 (0x1ffffffffffff) *)
@@ -1867,6 +1965,8 @@ Notation "'0b11111111111111111111111101111111111111111111111111'" (* 11258998732
:= (Const WO~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~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).
Notation "'0b11111111111111111111111111111111111111111110111110'" (* 1125899906842558 (0x3ffffffffffbe) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~0).
+Notation "'0b11111111111111111111111111111111111111111111010110'" (* 1125899906842582 (0x3ffffffffffd6) *)
+ := (Const WO~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~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1~0).
Notation "'0b11111111111111111111111111111111111111111111011010'" (* 1125899906842586 (0x3ffffffffffda) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
Notation "'0b11111111111111111111111111111111111111111111100001'" (* 1125899906842593 (0x3ffffffffffe1) *)
@@ -1917,6 +2017,8 @@ Notation "'0b111111111111111111111111111111111111111111111110111'" (* 2251799813
:= (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1).
Notation "'0b111111111111111111111111111111111111111111111111010'" (* 2251799813685242 (0x7fffffffffffa) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
+Notation "'0b111111111111111111111111111111111111111111111111101'" (* 2251799813685245 (0x7fffffffffffd) *)
+ := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1).
Notation "'0b111111111111111111111111111111111111111111111111110'" (* 2251799813685246 (0x7fffffffffffe) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0b111111111111111111111111111111111111111111111111111'" (* 2251799813685247 (0x7ffffffffffff) *)
@@ -1951,10 +2053,14 @@ Notation "'0b1111111111111111111111111111111111111111111111011010'" (* 450359962
:= (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
Notation "'0b1111111111111111111111111111111111111111111111011110'" (* 4503599627370462 (0xfffffffffffde) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
+Notation "'0b1111111111111111111111111111111111111111111111101011'" (* 4503599627370475 (0xfffffffffffeb) *)
+ := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1).
Notation "'0b1111111111111111111111111111111111111111111111101110'" (* 4503599627370478 (0xfffffffffffee) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0).
Notation "'0b1111111111111111111111111111111111111111111111101111'" (* 4503599627370479 (0xfffffffffffef) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
+Notation "'0b1111111111111111111111111111111111111111111111111010'" (* 4503599627370490 (0xffffffffffffa) *)
+ := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
Notation "'0b1111111111111111111111111111111111111111111111111011'" (* 4503599627370491 (0xffffffffffffb) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1).
Notation "'0b1111111111111111111111111111111111111111111111111110'" (* 4503599627370494 (0xffffffffffffe) *)
@@ -1977,8 +2083,14 @@ Notation "'0b11111111111111111111111111111111111111111111010000110'" (* 90071992
:= (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 "'0b11111111111111111111111111111111111111111111111010110'" (* 9007199254740950 (0x1fffffffffffd6) *)
+ := (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~0~1~0~1~1~0).
+Notation "'0b11111111111111111111111111111111111111111111111011110'" (* 9007199254740958 (0x1fffffffffffde) *)
+ := (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~0~1~1~1~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 "'0b11111111111111111111111111111111111111111111111100111'" (* 9007199254740967 (0x1fffffffffffe7) *)
+ := (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~1~1~1).
Notation "'0b11111111111111111111111111111111111111111111111110001'" (* 9007199254740977 (0x1ffffffffffff1) *)
:= (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~1~0~0~0~1).
Notation "'0b11111111111111111111111111111111111111111111111110110'" (* 9007199254740982 (0x1ffffffffffff6) *)
@@ -1995,6 +2107,8 @@ Notation "'0b100000000000000000000000000000000000000000000000000001'" (* 9007199
:= (Const WO~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~0~0~1).
Notation "'0b111111111111111111111111111111111111111111111111000110'" (* 18014398509481926 (0x3fffffffffffc6) *)
:= (Const WO~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~0).
+Notation "'0b111111111111111111111111111111111111111111111111001110'" (* 18014398509481934 (0x3fffffffffffce) *)
+ := (Const WO~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~1~1~1~0).
Notation "'0b111111111111111111111111111111111111111111111111100010'" (* 18014398509481954 (0x3fffffffffffe2) *)
:= (Const WO~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~1~0~0~0~1~0).
Notation "'0b111111111111111111111111111111111111111111111111110111'" (* 18014398509481975 (0x3ffffffffffff7) *)
@@ -2009,6 +2123,14 @@ 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 "'0b1111111111111111111111111111111111111111111111001011011'" (* 36028797018963547 (0x7ffffffffffe5b) *)
+ := (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~0~0~1~0~1~1~0~1~1).
+Notation "'0b1111111111111111111111111111111111111111111111011000011'" (* 36028797018963651 (0x7ffffffffffec3) *)
+ := (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~0~1~1~0~0~0~0~1~1).
+Notation "'0b1111111111111111111111111111111111111111111111101000101'" (* 36028797018963781 (0x7fffffffffff45) *)
+ := (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~0~1~0~0~0~1~0~1).
+Notation "'0b1111111111111111111111111111111111111111111111110010111'" (* 36028797018963863 (0x7fffffffffff97) *)
+ := (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~0~0~1~0~1~1~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) *)
@@ -2033,6 +2155,14 @@ Notation "'0b10000000000000000000000000000000000000000000000000000001'" (* 36028
:= (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~0~0~0~0~0~0~0~0~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 "'0b11111111111111110000000000000000000000000000000000000000'" (* 72056494526300160 (0xffff0000000000) *)
:= (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~0~0~0~0~0~0~0~0~0~0~0~0~0~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 "'0b11111111111111111111111111111111111111111111110010110110'" (* 72057594037927094 (0xfffffffffffcb6) *)
+ := (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~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~0).
+Notation "'0b11111111111111111111111111111111111111111111110110000110'" (* 72057594037927302 (0xfffffffffffd86) *)
+ := (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~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~0~0~0~1~1~0).
+Notation "'0b11111111111111111111111111111111111111111111111010001010'" (* 72057594037927562 (0xfffffffffffe8a) *)
+ := (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~1~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 "'0b11111111111111111111111111111111111111111111111100101110'" (* 72057594037927726 (0xffffffffffff2e) *)
+ := (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~1~1~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 "'0b11111111111111111111111111111111111111111111111110001011'" (* 72057594037927819 (0xffffffffffff8b) *)
:= (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~1~1~1~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~0~1~1).
Notation "'0b11111111111111111111111111111111111111111111111111000010'" (* 72057594037927874 (0xffffffffffffc2) *)
@@ -2043,6 +2173,8 @@ Notation "'0b11111111111111111111111111111111111111111111111111010110'" (* 72057
:= (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~1~1~1~1~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~0).
Notation "'0b11111111111111111111111111111111111111111111111111011010'" (* 72057594037927898 (0xffffffffffffda) *)
:= (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~1~1~1~1~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 "'0b11111111111111111111111111111111111111111111111111101011'" (* 72057594037927915 (0xffffffffffffeb) *)
+ := (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~1~1~1~1~1~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 "'0b11111111111111111111111111111111111111111111111111101111'" (* 72057594037927919 (0xffffffffffffef) *)
:= (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~1~1~1~1~1~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 "'0b11111111111111111111111111111111111111111111111111111011'" (* 72057594037927931 (0xfffffffffffffb) *)
@@ -2059,6 +2191,8 @@ Notation "'0b100000000000000000000000000000000000000000000000000000001'" (* 7205
:= (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~0~0~0~0~0~0~0~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 "'0b111111111111111111111111111111111111111111111111100010110'" (* 144115188075855638 (0x1ffffffffffff16) *)
:= (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~0~0~0~1~0~1~1~0).
+Notation "'0b111111111111111111111111111111111111111111111111111010110'" (* 144115188075855830 (0x1ffffffffffffd6) *)
+ := (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~0~1~0~1~1~0).
Notation "'0b111111111111111111111111111111111111111111111111111011110'" (* 144115188075855838 (0x1ffffffffffffde) *)
:= (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~0~1~1~1~1~0).
Notation "'0b111111111111111111111111111111111111111111111111111101101'" (* 144115188075855853 (0x1ffffffffffffed) *)
@@ -2087,6 +2221,8 @@ Notation "'0b1000000000000000000000000000000000000000000000000000000001'" (* 144
:= (Const WO~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~0~0~1).
Notation "'0b1111111111111111111111111111111111111111111111111111011010'" (* 288230376151711706 (0x3ffffffffffffda) *)
:= (Const WO~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~0~1~1~0~1~0).
+Notation "'0b1111111111111111111111111111111111111111111111111111100001'" (* 288230376151711713 (0x3ffffffffffffe1) *)
+ := (Const WO~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~0~0~0~1).
Notation "'0b1111111111111111111111111111111111111111111111111111100010'" (* 288230376151711714 (0x3ffffffffffffe2) *)
:= (Const WO~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~0~0~1~0).
Notation "'0b1111111111111111111111111111111111111111111111111111100101'" (* 288230376151711717 (0x3ffffffffffffe5) *)
@@ -2111,6 +2247,8 @@ Notation "'0b10000000000000000000000000000000000000000000000000000000000'" (* 28
:= (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~0~0~0~0~0~0~0~0~0~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 "'0b10000000000000000000000000000000000000000000000000000000001'" (* 288230376151711745 (0x400000000000001) *)
:= (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~0~0~0~0~0~0~0~0~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 "'0b11111111111111111111111111111111111111111111111111111000010'" (* 576460752303423426 (0x7ffffffffffffc2) *)
+ := (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~0~0~0~0~1~0).
Notation "'0b11111111111111111111111111111111111111111111111111111001010'" (* 576460752303423434 (0x7ffffffffffffca) *)
:= (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~0~0~1~0~1~0).
Notation "'0b11111111111111111111111111111111111111111111111111111011110'" (* 576460752303423454 (0x7ffffffffffffde) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index a1a8c9777..7f2102f97 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -18,6 +18,7 @@ nums = tuple(sorted(set(systematic_nums + [
187,
189,
317,
+ 421,
481,
569,
765,
@@ -141,7 +142,9 @@ nums = tuple(sorted(set(systematic_nums + [
33554427,
33554429,
33554430,
+ 67107887,
67108798,
+ 67108799,
67108826,
67108833,
67108839,
@@ -154,6 +157,8 @@ nums = tuple(sorted(set(systematic_nums + [
67108859,
67108861,
67108862,
+ 134215774,
+ 134217598,
134217666,
134217678,
134217690,
@@ -177,14 +182,17 @@ nums = tuple(sorted(set(systematic_nums + [
268435441,
268435443,
268435445,
+ 268435447,
268435451,
268435452,
268435453,
268435454,
+ 536869935,
536870882,
536870886,
536870890,
536870893,
+ 536870894,
536870902,
536870906,
536870907,
@@ -196,6 +204,7 @@ nums = tuple(sorted(set(systematic_nums + [
1054736383,
1065418751,
1073709055,
+ 1073739870,
1073741786,
1073741814,
1073741818,
@@ -249,6 +258,7 @@ nums = tuple(sorted(set(systematic_nums + [
4294967291,
4294967293,
4294967294,
+ 4294968273,
8589934559,
8589934567,
8589934575,
@@ -345,16 +355,20 @@ nums = tuple(sorted(set(systematic_nums + [
70368744177637,
70368744177647,
70368744177651,
+ 70368744177655,
70368744177658,
70368744177659,
+ 70368744177660,
70368744177661,
70368744177662,
140737471578110,
+ 140737479966719,
140737488355274,
140737488355294,
140737488355301,
140737488355302,
140737488355303,
+ 140737488355310,
140737488355313,
140737488355318,
140737488355319,
@@ -362,10 +376,15 @@ nums = tuple(sorted(set(systematic_nums + [
194613558116351,
281453501874175,
281470681743359,
+ 281474959933438,
281474976645119,
+ 281474976710235,
281474976710339,
+ 281474976710469,
+ 281474976710551,
281474976710602,
281474976710606,
+ 281474976710625,
281474976710626,
281474976710631,
281474976710637,
@@ -378,18 +397,26 @@ nums = tuple(sorted(set(systematic_nums + [
389227116232702,
562907003748350,
562949953290238,
+ 562949953420470,
562949953420678,
+ 562949953420938,
+ 562949953421102,
+ 562949953421250,
562949953421262,
562949953421274,
+ 562949953421278,
562949953421279,
562949953421290,
+ 562949953421291,
562949953421293,
562949953421294,
562949953421297,
562949953421303,
+ 562949953421306,
562949953421310,
1125899873288191,
1125899906842558,
+ 1125899906842582,
1125899906842586,
1125899906842593,
1125899906842594,
@@ -412,6 +439,7 @@ nums = tuple(sorted(set(systematic_nums + [
2251799813685238,
2251799813685239,
2251799813685242,
+ 2251799813685245,
2251799813685246,
2920302883373054,
4423885034356734,
@@ -426,8 +454,10 @@ nums = tuple(sorted(set(systematic_nums + [
4503599627370434,
4503599627370458,
4503599627370462,
+ 4503599627370475,
4503599627370478,
4503599627370479,
+ 4503599627370490,
4503599627370491,
4503599627370494,
9007190664804446,
@@ -436,16 +466,24 @@ nums = tuple(sorted(set(systematic_nums + [
9007199254740030,
9007199254740614,
9007199254740618,
+ 9007199254740950,
+ 9007199254740958,
9007199254740963,
+ 9007199254740967,
9007199254740977,
9007199254740982,
9007199254740988,
9007199254740990,
18014398509481926,
+ 18014398509481934,
18014398509481954,
18014398509481975,
18014398509481981,
18014398509481982,
+ 36028797018963547,
+ 36028797018963651,
+ 36028797018963781,
+ 36028797018963863,
36028797018963937,
36028797018963943,
36028797018963947,
@@ -455,16 +493,22 @@ nums = tuple(sorted(set(systematic_nums + [
36028797018963964,
36028797018963966,
72056494526300160,
+ 72057594037927094,
+ 72057594037927302,
+ 72057594037927562,
+ 72057594037927726,
72057594037927819,
72057594037927874,
72057594037927886,
72057594037927894,
72057594037927898,
+ 72057594037927915,
72057594037927919,
72057594037927931,
72057594037927933,
72057594037927934,
144115188075855638,
+ 144115188075855830,
144115188075855838,
144115188075855853,
144115188075855857,
@@ -476,6 +520,7 @@ nums = tuple(sorted(set(systematic_nums + [
144115188075855869,
144115188075855870,
288230376151711706,
+ 288230376151711713,
288230376151711714,
288230376151711717,
288230376151711726,
@@ -485,6 +530,7 @@ nums = tuple(sorted(set(systematic_nums + [
288230376151711740,
288230376151711741,
288230376151711742,
+ 576460752303423426,
576460752303423434,
576460752303423454,
576460752303423467,
@@ -1151,6 +1197,10 @@ Notation "'0x13d'" (* 317 (0x13d) *)
:= (Const 317%Z).
Notation "'0x13d'" (* 317 (0x13d) *)
:= (Const WO~0~0~0~0~0~0~0~1~0~0~1~1~1~1~0~1).
+Notation "'0x1a5'" (* 421 (0x1a5) *)
+ := (Const 421%Z).
+Notation "'0x1a5'" (* 421 (0x1a5) *)
+ := (Const WO~0~0~0~0~0~0~0~1~1~0~1~0~0~1~0~1).
Notation "'0x1e1'" (* 481 (0x1e1) *)
:= (Const 481%Z).
Notation "'0x1e1'" (* 481 (0x1e1) *)
@@ -1847,10 +1897,18 @@ Notation "'0x2000001'" (* 33554433 (0x2000001) *)
:= (Const 33554433%Z).
Notation "'0x2000001'" (* 33554433 (0x2000001) *)
:= (Const WO~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~1).
+Notation "'0x3fffc2f'" (* 67107887 (0x3fffc2f) *)
+ := (Const 67107887%Z).
+Notation "'0x3fffc2f'" (* 67107887 (0x3fffc2f) *)
+ := (Const WO~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~0~1~0~1~1~1~1).
Notation "'0x3ffffbe'" (* 67108798 (0x3ffffbe) *)
:= (Const 67108798%Z).
Notation "'0x3ffffbe'" (* 67108798 (0x3ffffbe) *)
:= (Const WO~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~0).
+Notation "'0x3ffffbf'" (* 67108799 (0x3ffffbf) *)
+ := (Const 67108799%Z).
+Notation "'0x3ffffbf'" (* 67108799 (0x3ffffbf) *)
+ := (Const WO~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).
Notation "'0x3ffffda'" (* 67108826 (0x3ffffda) *)
:= (Const 67108826%Z).
Notation "'0x3ffffda'" (* 67108826 (0x3ffffda) *)
@@ -1911,6 +1969,14 @@ Notation "'0x4000001'" (* 67108865 (0x4000001) *)
:= (Const 67108865%Z).
Notation "'0x4000001'" (* 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 "'0x7fff85e'" (* 134215774 (0x7fff85e) *)
+ := (Const 134215774%Z).
+Notation "'0x7fff85e'" (* 134215774 (0x7fff85e) *)
+ := (Const WO~0~0~0~0~0~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 "'0x7ffff7e'" (* 134217598 (0x7ffff7e) *)
+ := (Const 134217598%Z).
+Notation "'0x7ffff7e'" (* 134217598 (0x7ffff7e) *)
+ := (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~0~1~1~1~1~1~1~0).
Notation "'0x7ffffc2'" (* 134217666 (0x7ffffc2) *)
:= (Const 134217666%Z).
Notation "'0x7ffffc2'" (* 134217666 (0x7ffffc2) *)
@@ -2015,6 +2081,10 @@ Notation "'0xffffff5'" (* 268435445 (0xffffff5) *)
:= (Const 268435445%Z).
Notation "'0xffffff5'" (* 268435445 (0xffffff5) *)
:= (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~0~1~0~1).
+Notation "'0xffffff7'" (* 268435447 (0xffffff7) *)
+ := (Const 268435447%Z).
+Notation "'0xffffff7'" (* 268435447 (0xffffff7) *)
+ := (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~0~1~1~1).
Notation "'0xffffffb'" (* 268435451 (0xffffffb) *)
:= (Const 268435451%Z).
Notation "'0xffffffb'" (* 268435451 (0xffffffb) *)
@@ -2043,6 +2113,10 @@ Notation "'0x10000001'" (* 268435457 (0x10000001) *)
:= (Const 268435457%Z).
Notation "'0x10000001'" (* 268435457 (0x10000001) *)
:= (Const WO~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~1).
+Notation "'0x1ffffc2f'" (* 536869935 (0x1ffffc2f) *)
+ := (Const 536869935%Z).
+Notation "'0x1ffffc2f'" (* 536869935 (0x1ffffc2f) *)
+ := (Const WO~0~0~0~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 "'0x1fffffe2'" (* 536870882 (0x1fffffe2) *)
:= (Const 536870882%Z).
Notation "'0x1fffffe2'" (* 536870882 (0x1fffffe2) *)
@@ -2059,6 +2133,10 @@ Notation "'0x1fffffed'" (* 536870893 (0x1fffffed) *)
:= (Const 536870893%Z).
Notation "'0x1fffffed'" (* 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 "'0x1fffffee'" (* 536870894 (0x1fffffee) *)
+ := (Const 536870894%Z).
+Notation "'0x1fffffee'" (* 536870894 (0x1fffffee) *)
+ := (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~1~0).
Notation "'0x1ffffff6'" (* 536870902 (0x1ffffff6) *)
:= (Const 536870902%Z).
Notation "'0x1ffffff6'" (* 536870902 (0x1ffffff6) *)
@@ -2115,6 +2193,10 @@ Notation "'0x3fff7fff'" (* 1073709055 (0x3fff7fff) *)
:= (Const 1073709055%Z).
Notation "'0x3fff7fff'" (* 1073709055 (0x3fff7fff) *)
:= (Const WO~0~0~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).
+Notation "'0x3ffff85e'" (* 1073739870 (0x3ffff85e) *)
+ := (Const 1073739870%Z).
+Notation "'0x3ffff85e'" (* 1073739870 (0x3ffff85e) *)
+ := (Const WO~0~0~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 "'0x3fffffda'" (* 1073741786 (0x3fffffda) *)
:= (Const 1073741786%Z).
Notation "'0x3fffffda'" (* 1073741786 (0x3fffffda) *)
@@ -2359,6 +2441,10 @@ Notation "'0x100000001'" (* 4294967297 (0x100000001) *)
:= (Const 4294967297%Z).
Notation "'0x100000001'" (* 4294967297 (0x100000001) *)
:= (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~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~1).
+Notation "'0x1000003d1'" (* 4294968273 (0x1000003d1) *)
+ := (Const 4294968273%Z).
+Notation "'0x1000003d1'" (* 4294968273 (0x1000003d1) *)
+ := (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~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~1~1~1~0~1~0~0~0~1).
Notation "'0x1ffffffdf'" (* 8589934559 (0x1ffffffdf) *)
:= (Const 8589934559%Z).
Notation "'0x1ffffffdf'" (* 8589934559 (0x1ffffffdf) *)
@@ -2899,6 +2985,10 @@ Notation "'0x3ffffffffff3'" (* 70368744177651 (0x3ffffffffff3) *)
:= (Const 70368744177651%Z).
Notation "'0x3ffffffffff3'" (* 70368744177651 (0x3ffffffffff3) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~0~0~1~1).
+Notation "'0x3ffffffffff7'" (* 70368744177655 (0x3ffffffffff7) *)
+ := (Const 70368744177655%Z).
+Notation "'0x3ffffffffff7'" (* 70368744177655 (0x3ffffffffff7) *)
+ := (Const WO~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~1~1~1~1~1~1~1~1~0~1~1~1).
Notation "'0x3ffffffffffa'" (* 70368744177658 (0x3ffffffffffa) *)
:= (Const 70368744177658%Z).
Notation "'0x3ffffffffffa'" (* 70368744177658 (0x3ffffffffffa) *)
@@ -2907,6 +2997,10 @@ Notation "'0x3ffffffffffb'" (* 70368744177659 (0x3ffffffffffb) *)
:= (Const 70368744177659%Z).
Notation "'0x3ffffffffffb'" (* 70368744177659 (0x3ffffffffffb) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~1~0~1~1).
+Notation "'0x3ffffffffffc'" (* 70368744177660 (0x3ffffffffffc) *)
+ := (Const 70368744177660%Z).
+Notation "'0x3ffffffffffc'" (* 70368744177660 (0x3ffffffffffc) *)
+ := (Const WO~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~1~1~1~1~1~1~1~1~1~1~0~0).
Notation "'0x3ffffffffffd'" (* 70368744177661 (0x3ffffffffffd) *)
:= (Const 70368744177661%Z).
Notation "'0x3ffffffffffd'" (* 70368744177661 (0x3ffffffffffd) *)
@@ -2931,6 +3025,10 @@ Notation "'0x7ffffefffffe'" (* 140737471578110 (0x7ffffefffffe) *)
:= (Const 140737471578110%Z).
Notation "'0x7ffffefffffe'" (* 140737471578110 (0x7ffffefffffe) *)
:= (Const WO~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~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).
+Notation "'0x7fffff7fffff'" (* 140737479966719 (0x7fffff7fffff) *)
+ := (Const 140737479966719%Z).
+Notation "'0x7fffff7fffff'" (* 140737479966719 (0x7fffff7fffff) *)
+ := (Const WO~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~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
Notation "'0x7fffffffffca'" (* 140737488355274 (0x7fffffffffca) *)
:= (Const 140737488355274%Z).
Notation "'0x7fffffffffca'" (* 140737488355274 (0x7fffffffffca) *)
@@ -2951,6 +3049,10 @@ Notation "'0x7fffffffffe7'" (* 140737488355303 (0x7fffffffffe7) *)
:= (Const 140737488355303%Z).
Notation "'0x7fffffffffe7'" (* 140737488355303 (0x7fffffffffe7) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~0~0~1~1~1).
+Notation "'0x7fffffffffee'" (* 140737488355310 (0x7fffffffffee) *)
+ := (Const 140737488355310%Z).
+Notation "'0x7fffffffffee'" (* 140737488355310 (0x7fffffffffee) *)
+ := (Const WO~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~1~1~1~1~1~1~1~1~0~1~1~1~0).
Notation "'0x7ffffffffff1'" (* 140737488355313 (0x7ffffffffff1) *)
:= (Const 140737488355313%Z).
Notation "'0x7ffffffffff1'" (* 140737488355313 (0x7ffffffffff1) *)
@@ -2991,14 +3093,30 @@ Notation "'0xfffeffffffff'" (* 281470681743359 (0xfffeffffffff) *)
:= (Const 281470681743359%Z).
Notation "'0xfffeffffffff'" (* 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 "'0xfffffefffffe'" (* 281474959933438 (0xfffffefffffe) *)
+ := (Const 281474959933438%Z).
+Notation "'0xfffffefffffe'" (* 281474959933438 (0xfffffefffffe) *)
+ := (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~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~0).
Notation "'0xfffffffeffff'" (* 281474976645119 (0xfffffffeffff) *)
:= (Const 281474976645119%Z).
Notation "'0xfffffffeffff'" (* 281474976645119 (0xfffffffeffff) *)
:= (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~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 "'0xfffffffffe5b'" (* 281474976710235 (0xfffffffffe5b) *)
+ := (Const 281474976710235%Z).
+Notation "'0xfffffffffe5b'" (* 281474976710235 (0xfffffffffe5b) *)
+ := (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~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 "'0xfffffffffec3'" (* 281474976710339 (0xfffffffffec3) *)
:= (Const 281474976710339%Z).
Notation "'0xfffffffffec3'" (* 281474976710339 (0xfffffffffec3) *)
:= (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~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~0~0~0~1~1).
+Notation "'0xffffffffff45'" (* 281474976710469 (0xffffffffff45) *)
+ := (Const 281474976710469%Z).
+Notation "'0xffffffffff45'" (* 281474976710469 (0xffffffffff45) *)
+ := (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~1~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).
+Notation "'0xffffffffff97'" (* 281474976710551 (0xffffffffff97) *)
+ := (Const 281474976710551%Z).
+Notation "'0xffffffffff97'" (* 281474976710551 (0xffffffffff97) *)
+ := (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~1~1~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).
Notation "'0xffffffffffca'" (* 281474976710602 (0xffffffffffca) *)
:= (Const 281474976710602%Z).
Notation "'0xffffffffffca'" (* 281474976710602 (0xffffffffffca) *)
@@ -3007,6 +3125,10 @@ Notation "'0xffffffffffce'" (* 281474976710606 (0xffffffffffce) *)
:= (Const 281474976710606%Z).
Notation "'0xffffffffffce'" (* 281474976710606 (0xffffffffffce) *)
:= (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~1~1~1~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~0).
+Notation "'0xffffffffffe1'" (* 281474976710625 (0xffffffffffe1) *)
+ := (Const 281474976710625%Z).
+Notation "'0xffffffffffe1'" (* 281474976710625 (0xffffffffffe1) *)
+ := (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~1~1~1~1~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 "'0xffffffffffe2'" (* 281474976710626 (0xffffffffffe2) *)
:= (Const 281474976710626%Z).
Notation "'0xffffffffffe2'" (* 281474976710626 (0xffffffffffe2) *)
@@ -3067,10 +3189,26 @@ Notation "'0x1fffffffdfffe'" (* 562949953290238 (0x1fffffffdfffe) *)
:= (Const 562949953290238%Z).
Notation "'0x1fffffffdfffe'" (* 562949953290238 (0x1fffffffdfffe) *)
:= (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~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~0).
+Notation "'0x1fffffffffcb6'" (* 562949953420470 (0x1fffffffffcb6) *)
+ := (Const 562949953420470%Z).
+Notation "'0x1fffffffffcb6'" (* 562949953420470 (0x1fffffffffcb6) *)
+ := (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~1~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~0).
Notation "'0x1fffffffffd86'" (* 562949953420678 (0x1fffffffffd86) *)
:= (Const 562949953420678%Z).
Notation "'0x1fffffffffd86'" (* 562949953420678 (0x1fffffffffd86) *)
:= (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~1~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~0~0~0~1~1~0).
+Notation "'0x1fffffffffe8a'" (* 562949953420938 (0x1fffffffffe8a) *)
+ := (Const 562949953420938%Z).
+Notation "'0x1fffffffffe8a'" (* 562949953420938 (0x1fffffffffe8a) *)
+ := (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~1~1~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 "'0x1ffffffffff2e'" (* 562949953421102 (0x1ffffffffff2e) *)
+ := (Const 562949953421102%Z).
+Notation "'0x1ffffffffff2e'" (* 562949953421102 (0x1ffffffffff2e) *)
+ := (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~1~1~1~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 "'0x1ffffffffffc2'" (* 562949953421250 (0x1ffffffffffc2) *)
+ := (Const 562949953421250%Z).
+Notation "'0x1ffffffffffc2'" (* 562949953421250 (0x1ffffffffffc2) *)
+ := (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~1~1~1~1~1~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~0).
Notation "'0x1ffffffffffce'" (* 562949953421262 (0x1ffffffffffce) *)
:= (Const 562949953421262%Z).
Notation "'0x1ffffffffffce'" (* 562949953421262 (0x1ffffffffffce) *)
@@ -3079,6 +3217,10 @@ Notation "'0x1ffffffffffda'" (* 562949953421274 (0x1ffffffffffda) *)
:= (Const 562949953421274%Z).
Notation "'0x1ffffffffffda'" (* 562949953421274 (0x1ffffffffffda) *)
:= (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~1~1~1~1~1~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 "'0x1ffffffffffde'" (* 562949953421278 (0x1ffffffffffde) *)
+ := (Const 562949953421278%Z).
+Notation "'0x1ffffffffffde'" (* 562949953421278 (0x1ffffffffffde) *)
+ := (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~1~1~1~1~1~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~0).
Notation "'0x1ffffffffffdf'" (* 562949953421279 (0x1ffffffffffdf) *)
:= (Const 562949953421279%Z).
Notation "'0x1ffffffffffdf'" (* 562949953421279 (0x1ffffffffffdf) *)
@@ -3087,6 +3229,10 @@ Notation "'0x1ffffffffffea'" (* 562949953421290 (0x1ffffffffffea) *)
:= (Const 562949953421290%Z).
Notation "'0x1ffffffffffea'" (* 562949953421290 (0x1ffffffffffea) *)
:= (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~1~1~1~1~1~1~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~0).
+Notation "'0x1ffffffffffeb'" (* 562949953421291 (0x1ffffffffffeb) *)
+ := (Const 562949953421291%Z).
+Notation "'0x1ffffffffffeb'" (* 562949953421291 (0x1ffffffffffeb) *)
+ := (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~1~1~1~1~1~1~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 "'0x1ffffffffffed'" (* 562949953421293 (0x1ffffffffffed) *)
:= (Const 562949953421293%Z).
Notation "'0x1ffffffffffed'" (* 562949953421293 (0x1ffffffffffed) *)
@@ -3103,6 +3249,10 @@ Notation "'0x1fffffffffff7'" (* 562949953421303 (0x1fffffffffff7) *)
:= (Const 562949953421303%Z).
Notation "'0x1fffffffffff7'" (* 562949953421303 (0x1fffffffffff7) *)
:= (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~1~1~1~1~1~1~1~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 "'0x1fffffffffffa'" (* 562949953421306 (0x1fffffffffffa) *)
+ := (Const 562949953421306%Z).
+Notation "'0x1fffffffffffa'" (* 562949953421306 (0x1fffffffffffa) *)
+ := (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~1~1~1~1~1~1~1~1~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 "'0x1fffffffffffe'" (* 562949953421310 (0x1fffffffffffe) *)
:= (Const 562949953421310%Z).
Notation "'0x1fffffffffffe'" (* 562949953421310 (0x1fffffffffffe) *)
@@ -3127,6 +3277,10 @@ Notation "'0x3ffffffffffbe'" (* 1125899906842558 (0x3ffffffffffbe) *)
:= (Const 1125899906842558%Z).
Notation "'0x3ffffffffffbe'" (* 1125899906842558 (0x3ffffffffffbe) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~0).
+Notation "'0x3ffffffffffd6'" (* 1125899906842582 (0x3ffffffffffd6) *)
+ := (Const 1125899906842582%Z).
+Notation "'0x3ffffffffffd6'" (* 1125899906842582 (0x3ffffffffffd6) *)
+ := (Const WO~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~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1~0).
Notation "'0x3ffffffffffda'" (* 1125899906842586 (0x3ffffffffffda) *)
:= (Const 1125899906842586%Z).
Notation "'0x3ffffffffffda'" (* 1125899906842586 (0x3ffffffffffda) *)
@@ -3227,6 +3381,10 @@ Notation "'0x7fffffffffffa'" (* 2251799813685242 (0x7fffffffffffa) *)
:= (Const 2251799813685242%Z).
Notation "'0x7fffffffffffa'" (* 2251799813685242 (0x7fffffffffffa) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
+Notation "'0x7fffffffffffd'" (* 2251799813685245 (0x7fffffffffffd) *)
+ := (Const 2251799813685245%Z).
+Notation "'0x7fffffffffffd'" (* 2251799813685245 (0x7fffffffffffd) *)
+ := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1).
Notation "'0x7fffffffffffe'" (* 2251799813685246 (0x7fffffffffffe) *)
:= (Const 2251799813685246%Z).
Notation "'0x7fffffffffffe'" (* 2251799813685246 (0x7fffffffffffe) *)
@@ -3295,6 +3453,10 @@ Notation "'0xfffffffffffde'" (* 4503599627370462 (0xfffffffffffde) *)
:= (Const 4503599627370462%Z).
Notation "'0xfffffffffffde'" (* 4503599627370462 (0xfffffffffffde) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
+Notation "'0xfffffffffffeb'" (* 4503599627370475 (0xfffffffffffeb) *)
+ := (Const 4503599627370475%Z).
+Notation "'0xfffffffffffeb'" (* 4503599627370475 (0xfffffffffffeb) *)
+ := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1).
Notation "'0xfffffffffffee'" (* 4503599627370478 (0xfffffffffffee) *)
:= (Const 4503599627370478%Z).
Notation "'0xfffffffffffee'" (* 4503599627370478 (0xfffffffffffee) *)
@@ -3303,6 +3465,10 @@ Notation "'0xfffffffffffef'" (* 4503599627370479 (0xfffffffffffef) *)
:= (Const 4503599627370479%Z).
Notation "'0xfffffffffffef'" (* 4503599627370479 (0xfffffffffffef) *)
:= (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
+Notation "'0xffffffffffffa'" (* 4503599627370490 (0xffffffffffffa) *)
+ := (Const 4503599627370490%Z).
+Notation "'0xffffffffffffa'" (* 4503599627370490 (0xffffffffffffa) *)
+ := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
Notation "'0xffffffffffffb'" (* 4503599627370491 (0xffffffffffffb) *)
:= (Const 4503599627370491%Z).
Notation "'0xffffffffffffb'" (* 4503599627370491 (0xffffffffffffb) *)
@@ -3347,10 +3513,22 @@ 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 "'0x1fffffffffffd6'" (* 9007199254740950 (0x1fffffffffffd6) *)
+ := (Const 9007199254740950%Z).
+Notation "'0x1fffffffffffd6'" (* 9007199254740950 (0x1fffffffffffd6) *)
+ := (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~0~1~0~1~1~0).
+Notation "'0x1fffffffffffde'" (* 9007199254740958 (0x1fffffffffffde) *)
+ := (Const 9007199254740958%Z).
+Notation "'0x1fffffffffffde'" (* 9007199254740958 (0x1fffffffffffde) *)
+ := (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~0~1~1~1~1~0).
Notation "'0x1fffffffffffe3'" (* 9007199254740963 (0x1fffffffffffe3) *)
:= (Const 9007199254740963%Z).
Notation "'0x1fffffffffffe3'" (* 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 "'0x1fffffffffffe7'" (* 9007199254740967 (0x1fffffffffffe7) *)
+ := (Const 9007199254740967%Z).
+Notation "'0x1fffffffffffe7'" (* 9007199254740967 (0x1fffffffffffe7) *)
+ := (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~1~1~1).
Notation "'0x1ffffffffffff1'" (* 9007199254740977 (0x1ffffffffffff1) *)
:= (Const 9007199254740977%Z).
Notation "'0x1ffffffffffff1'" (* 9007199254740977 (0x1ffffffffffff1) *)
@@ -3383,6 +3561,10 @@ Notation "'0x3fffffffffffc6'" (* 18014398509481926 (0x3fffffffffffc6) *)
:= (Const 18014398509481926%Z).
Notation "'0x3fffffffffffc6'" (* 18014398509481926 (0x3fffffffffffc6) *)
:= (Const WO~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~0).
+Notation "'0x3fffffffffffce'" (* 18014398509481934 (0x3fffffffffffce) *)
+ := (Const 18014398509481934%Z).
+Notation "'0x3fffffffffffce'" (* 18014398509481934 (0x3fffffffffffce) *)
+ := (Const WO~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~1~1~1~0).
Notation "'0x3fffffffffffe2'" (* 18014398509481954 (0x3fffffffffffe2) *)
:= (Const 18014398509481954%Z).
Notation "'0x3fffffffffffe2'" (* 18014398509481954 (0x3fffffffffffe2) *)
@@ -3411,6 +3593,22 @@ 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 "'0x7ffffffffffe5b'" (* 36028797018963547 (0x7ffffffffffe5b) *)
+ := (Const 36028797018963547%Z).
+Notation "'0x7ffffffffffe5b'" (* 36028797018963547 (0x7ffffffffffe5b) *)
+ := (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~0~0~1~0~1~1~0~1~1).
+Notation "'0x7ffffffffffec3'" (* 36028797018963651 (0x7ffffffffffec3) *)
+ := (Const 36028797018963651%Z).
+Notation "'0x7ffffffffffec3'" (* 36028797018963651 (0x7ffffffffffec3) *)
+ := (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~0~1~1~0~0~0~0~1~1).
+Notation "'0x7fffffffffff45'" (* 36028797018963781 (0x7fffffffffff45) *)
+ := (Const 36028797018963781%Z).
+Notation "'0x7fffffffffff45'" (* 36028797018963781 (0x7fffffffffff45) *)
+ := (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~0~1~0~0~0~1~0~1).
+Notation "'0x7fffffffffff97'" (* 36028797018963863 (0x7fffffffffff97) *)
+ := (Const 36028797018963863%Z).
+Notation "'0x7fffffffffff97'" (* 36028797018963863 (0x7fffffffffff97) *)
+ := (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~0~0~1~0~1~1~1).
Notation "'0x7fffffffffffe1'" (* 36028797018963937 (0x7fffffffffffe1) *)
:= (Const 36028797018963937%Z).
Notation "'0x7fffffffffffe1'" (* 36028797018963937 (0x7fffffffffffe1) *)
@@ -3459,6 +3657,22 @@ Notation "'0xffff0000000000'" (* 72056494526300160 (0xffff0000000000) *)
:= (Const 72056494526300160%Z).
Notation "'0xffff0000000000'" (* 72056494526300160 (0xffff0000000000) *)
:= (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~0~0~0~0~0~0~0~0~0~0~0~0~0~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 "'0xfffffffffffcb6'" (* 72057594037927094 (0xfffffffffffcb6) *)
+ := (Const 72057594037927094%Z).
+Notation "'0xfffffffffffcb6'" (* 72057594037927094 (0xfffffffffffcb6) *)
+ := (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~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~0).
+Notation "'0xfffffffffffd86'" (* 72057594037927302 (0xfffffffffffd86) *)
+ := (Const 72057594037927302%Z).
+Notation "'0xfffffffffffd86'" (* 72057594037927302 (0xfffffffffffd86) *)
+ := (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~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~0~0~0~1~1~0).
+Notation "'0xfffffffffffe8a'" (* 72057594037927562 (0xfffffffffffe8a) *)
+ := (Const 72057594037927562%Z).
+Notation "'0xfffffffffffe8a'" (* 72057594037927562 (0xfffffffffffe8a) *)
+ := (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~1~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 "'0xffffffffffff2e'" (* 72057594037927726 (0xffffffffffff2e) *)
+ := (Const 72057594037927726%Z).
+Notation "'0xffffffffffff2e'" (* 72057594037927726 (0xffffffffffff2e) *)
+ := (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~1~1~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 "'0xffffffffffff8b'" (* 72057594037927819 (0xffffffffffff8b) *)
:= (Const 72057594037927819%Z).
Notation "'0xffffffffffff8b'" (* 72057594037927819 (0xffffffffffff8b) *)
@@ -3479,6 +3693,10 @@ Notation "'0xffffffffffffda'" (* 72057594037927898 (0xffffffffffffda) *)
:= (Const 72057594037927898%Z).
Notation "'0xffffffffffffda'" (* 72057594037927898 (0xffffffffffffda) *)
:= (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~1~1~1~1~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 "'0xffffffffffffeb'" (* 72057594037927915 (0xffffffffffffeb) *)
+ := (Const 72057594037927915%Z).
+Notation "'0xffffffffffffeb'" (* 72057594037927915 (0xffffffffffffeb) *)
+ := (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~1~1~1~1~1~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 "'0xffffffffffffef'" (* 72057594037927919 (0xffffffffffffef) *)
:= (Const 72057594037927919%Z).
Notation "'0xffffffffffffef'" (* 72057594037927919 (0xffffffffffffef) *)
@@ -3511,6 +3729,10 @@ Notation "'0x1ffffffffffff16'" (* 144115188075855638 (0x1ffffffffffff16) *)
:= (Const 144115188075855638%Z).
Notation "'0x1ffffffffffff16'" (* 144115188075855638 (0x1ffffffffffff16) *)
:= (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~0~0~0~1~0~1~1~0).
+Notation "'0x1ffffffffffffd6'" (* 144115188075855830 (0x1ffffffffffffd6) *)
+ := (Const 144115188075855830%Z).
+Notation "'0x1ffffffffffffd6'" (* 144115188075855830 (0x1ffffffffffffd6) *)
+ := (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~0~1~0~1~1~0).
Notation "'0x1ffffffffffffde'" (* 144115188075855838 (0x1ffffffffffffde) *)
:= (Const 144115188075855838%Z).
Notation "'0x1ffffffffffffde'" (* 144115188075855838 (0x1ffffffffffffde) *)
@@ -3567,6 +3789,10 @@ Notation "'0x3ffffffffffffda'" (* 288230376151711706 (0x3ffffffffffffda) *)
:= (Const 288230376151711706%Z).
Notation "'0x3ffffffffffffda'" (* 288230376151711706 (0x3ffffffffffffda) *)
:= (Const WO~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~0~1~1~0~1~0).
+Notation "'0x3ffffffffffffe1'" (* 288230376151711713 (0x3ffffffffffffe1) *)
+ := (Const 288230376151711713%Z).
+Notation "'0x3ffffffffffffe1'" (* 288230376151711713 (0x3ffffffffffffe1) *)
+ := (Const WO~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~0~0~0~1).
Notation "'0x3ffffffffffffe2'" (* 288230376151711714 (0x3ffffffffffffe2) *)
:= (Const 288230376151711714%Z).
Notation "'0x3ffffffffffffe2'" (* 288230376151711714 (0x3ffffffffffffe2) *)
@@ -3615,6 +3841,10 @@ Notation "'0x400000000000001'" (* 288230376151711745 (0x400000000000001) *)
:= (Const 288230376151711745%Z).
Notation "'0x400000000000001'" (* 288230376151711745 (0x400000000000001) *)
:= (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~0~0~0~0~0~0~0~0~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 "'0x7ffffffffffffc2'" (* 576460752303423426 (0x7ffffffffffffc2) *)
+ := (Const 576460752303423426%Z).
+Notation "'0x7ffffffffffffc2'" (* 576460752303423426 (0x7ffffffffffffc2) *)
+ := (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~0~0~0~0~1~0).
Notation "'0x7ffffffffffffca'" (* 576460752303423434 (0x7ffffffffffffca) *)
:= (Const 576460752303423434%Z).
Notation "'0x7ffffffffffffca'" (* 576460752303423434 (0x7ffffffffffffca) *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-21 10:02:06 +0000