aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-11-13 00:51:13 -0500
committerGravatar Jason Gross <jgross@mit.edu>2017-11-13 00:51:13 -0500
commit2d411951867e21c821bda7ca2a4edee30c13cf3b (patch)
treef22afa6a3d7e202c333c2674ab938b33a647abc1
parent3aeb16c84f1554a5b6d4e63d5b417e1829bfbf18 (diff)
Add more constant notations
Diffstat
-rw-r--r--src/Compilers/Z/BinaryNotationConstants.v111
-rw-r--r--src/Compilers/Z/HexNotationConstants.v185
2 files changed, 296 insertions, 0 deletions
diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 51bfa3c77..7c73cd8d2 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -42,6 +42,7 @@ nums = tuple(sorted(set(systematic_nums + [
262142,
523807,
524101,
+ 524223,
524262,
524263,
524267,
@@ -51,9 +52,14 @@ nums = tuple(sorted(set(systematic_nums + [
524279,
524286,
679935,
+ 1032192,
+ 1044479,
+ 1047599,
1047811,
1048202,
+ 1048446,
1048471,
+ 1048511,
1048526,
1048534,
1048538,
@@ -65,8 +71,11 @@ nums = tuple(sorted(set(systematic_nums + [
1048574,
1359870,
2060031,
+ 2064384,
2081439,
+ 2088958,
2094335,
+ 2095198,
2095622,
2096127,
2096128,
@@ -85,8 +94,10 @@ nums = tuple(sorted(set(systematic_nums + [
4193327,
4193539,
4193735,
+ 4193883,
4193987,
4194115,
+ 4194240,
4194254,
4194270,
4194271,
@@ -101,11 +112,16 @@ nums = tuple(sorted(set(systematic_nums + [
4194301,
4194302,
8323583,
+ 8372224,
8386654,
8387078,
8387470,
+ 8387766,
8387974,
+ 8388187,
8388230,
+ 8388291,
+ 8388421,
8388491,
8388503,
8388542,
@@ -129,6 +145,9 @@ nums = tuple(sorted(set(systematic_nums + [
16647166,
16711679,
16775935,
+ 16776374,
+ 16776582,
+ 16776842,
16776959,
16776982,
16777006,
@@ -137,6 +156,7 @@ nums = tuple(sorted(set(systematic_nums + [
16777111,
16777162,
16777182,
+ 16777185,
16777186,
16777187,
16777189,
@@ -158,17 +178,21 @@ nums = tuple(sorted(set(systematic_nums + [
33423358,
33551870,
33554054,
+ 33554058,
33554222,
33554315,
+ 33554370,
33554374,
33554378,
33554382,
33554394,
33554398,
33554399,
+ 33554401,
33554402,
33554407,
33554410,
+ 33554411,
33554413,
33554414,
33554415,
@@ -177,19 +201,23 @@ nums = tuple(sorted(set(systematic_nums + [
33554423,
33554426,
33554427,
+ 33554428,
33554429,
33554430,
67107887,
67108630,
67108798,
67108799,
+ 67108802,
67108814,
+ 67108822,
67108826,
67108830,
67108833,
67108834,
67108837,
67108839,
+ 67108843,
67108845,
67108846,
67108847,
@@ -198,6 +226,7 @@ nums = tuple(sorted(set(systematic_nums + [
67108855,
67108858,
67108859,
+ 67108860,
67108861,
67108862,
134215774,
@@ -205,6 +234,7 @@ nums = tuple(sorted(set(systematic_nums + [
134217666,
134217674,
134217678,
+ 134217686,
134217690,
134217694,
134217697,
@@ -213,6 +243,7 @@ nums = tuple(sorted(set(systematic_nums + [
134217703,
134217709,
134217710,
+ 134217711,
134217713,
134217718,
134217719,
@@ -225,6 +256,7 @@ nums = tuple(sorted(set(systematic_nums + [
268435398,
268435406,
268435418,
+ 268435422,
268435426,
268435438,
268435441,
@@ -326,12 +358,16 @@ nums = tuple(sorted(set(systematic_nums + [
68719476727,
68719476733,
68719476734,
+ 133143985199,
137436856320,
137438952991,
137438953285,
137438953355,
137438953454,
+ 137438953470,
+ 266287970398,
274844352511,
+ 274877902847,
274877906919,
274877906927,
274877906933,
@@ -339,6 +375,7 @@ nums = tuple(sorted(set(systematic_nums + [
274877906941,
274877906942,
549688705022,
+ 549755289600,
549755813783,
549755813838,
549755813854,
@@ -1094,6 +1131,8 @@ Notation "'0b1111111111000011111'" (* 523807 (0x7fe1f) *)
:= (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~0~0~0~0~1~1~1~1~1).
Notation "'0b1111111111101000101'" (* 524101 (0x7ff45) *)
:= (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~0~1~0~0~0~1~0~1).
+Notation "'0b1111111111110111111'" (* 524223 (0x7ffbf) *)
+ := (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~0~1~1~1~1~1~1).
Notation "'0b1111111111111100110'" (* 524262 (0x7ffe6) *)
:= (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~0~0~1~1~0).
Notation "'0b1111111111111100111'" (* 524263 (0x7ffe7) *)
@@ -1118,12 +1157,22 @@ Notation "'0b10000000000000000001'" (* 524289 (0x80001) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
Notation "'0b10100101111111111111'" (* 679935 (0xa5fff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0b11111100000000000000'" (* 1032192 (0xfc000) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
+Notation "'0b11111110111111111111'" (* 1044479 (0xfefff) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0b11111111110000101111'" (* 1047599 (0xffc2f) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1).
Notation "'0b11111111110100000011'" (* 1047811 (0xffd03) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~0~0~1~1).
Notation "'0b11111111111010001010'" (* 1048202 (0xffe8a) *)
:= (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~0~1~0~0~0~1~0~1~0).
+Notation "'0b11111111111101111110'" (* 1048446 (0xfff7e) *)
+ := (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~0~1~1~1~1~1~1~0).
Notation "'0b11111111111110010111'" (* 1048471 (0xfff97) *)
:= (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~0~0~1~0~1~1~1).
+Notation "'0b11111111111110111111'" (* 1048511 (0xfffbf) *)
+ := (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~0~1~1~1~1~1~1).
Notation "'0b11111111111111001110'" (* 1048526 (0xfffce) *)
:= (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~0~0~1~1~1~0).
Notation "'0b11111111111111010110'" (* 1048534 (0xfffd6) *)
@@ -1152,10 +1201,16 @@ Notation "'0b101001011111111111110'" (* 1359870 (0x14bffe) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0b111110110111011111111'" (* 2060031 (0x1f6eff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~0~1~1~0~1~1~1~0~1~1~1~1~1~1~1~1).
+Notation "'0b111111000000000000000'" (* 2064384 (0x1f8000) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
Notation "'0b111111100001010011111'" (* 2081439 (0x1fc29f) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~0~0~0~1~0~1~0~0~1~1~1~1~1).
+Notation "'0b111111101111111111110'" (* 2088958 (0x1fdffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0b111111111010011111111'" (* 2094335 (0x1ff4ff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~0~1~0~0~1~1~1~1~1~1~1~1).
+Notation "'0b111111111100001011110'" (* 2095198 (0x1ff85e) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1~0).
Notation "'0b111111111101000000110'" (* 2095622 (0x1ffa06) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~0~0~1~1~0).
Notation "'0b111111111101111111111'" (* 2096127 (0x1ffbff) *)
@@ -1198,10 +1253,14 @@ Notation "'0b1111111111110100000011'" (* 4193539 (0x3ffd03) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~0~0~1~1).
Notation "'0b1111111111110111000111'" (* 4193735 (0x3ffdc7) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1).
+Notation "'0b1111111111111001011011'" (* 4193883 (0x3ffe5b) *)
+ := (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~0~0~1~0~1~1~0~1~1).
Notation "'0b1111111111111011000011'" (* 4193987 (0x3ffec3) *)
:= (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~0~1~1~0~0~0~0~1~1).
Notation "'0b1111111111111101000011'" (* 4194115 (0x3fff43) *)
:= (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~0~1~0~0~0~0~1~1).
+Notation "'0b1111111111111111000000'" (* 4194240 (0x3fffc0) *)
+ := (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~0~0~0~0~0~0).
Notation "'0b1111111111111111001110'" (* 4194254 (0x3fffce) *)
:= (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~0~0~1~1~1~0).
Notation "'0b1111111111111111011110'" (* 4194270 (0x3fffde) *)
@@ -1236,16 +1295,26 @@ Notation "'0b10000000000000000000001'" (* 4194305 (0x400001) *)
:= (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~1).
Notation "'0b11111110000000111111111'" (* 8323583 (0x7f01ff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1).
+Notation "'0b11111111100000000000000'" (* 8372224 (0x7fc000) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
Notation "'0b11111111111100001011110'" (* 8386654 (0x7ff85e) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1~0).
Notation "'0b11111111111101000000110'" (* 8387078 (0x7ffa06) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~0~0~1~1~0).
Notation "'0b11111111111101110001110'" (* 8387470 (0x7ffb8e) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1~0).
+Notation "'0b11111111111110010110110'" (* 8387766 (0x7ffcb6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~0~1~1~0).
Notation "'0b11111111111110110000110'" (* 8387974 (0x7ffd86) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~0~0~0~1~1~0).
+Notation "'0b11111111111111001011011'" (* 8388187 (0x7ffe5b) *)
+ := (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~0~0~1~0~1~1~0~1~1).
Notation "'0b11111111111111010000110'" (* 8388230 (0x7ffe86) *)
:= (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~0~1~0~0~0~0~1~1~0).
+Notation "'0b11111111111111011000011'" (* 8388291 (0x7ffec3) *)
+ := (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~0~1~1~0~0~0~0~1~1).
+Notation "'0b11111111111111101000101'" (* 8388421 (0x7fff45) *)
+ := (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~0~1~0~0~0~1~0~1).
Notation "'0b11111111111111110001011'" (* 8388491 (0x7fff8b) *)
:= (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~0~0~0~1~0~1~1).
Notation "'0b11111111111111110010111'" (* 8388503 (0x7fff97) *)
@@ -1298,6 +1367,12 @@ Notation "'0b111111101111111111111111'" (* 16711679 (0xfeffff) *)
:= (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
Notation "'0b111111111111101011111111'" (* 16775935 (0xfffaff) *)
:= (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1~1~1~1~1~1~1).
+Notation "'0b111111111111110010110110'" (* 16776374 (0xfffcb6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~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 "'0b111111111111110110000110'" (* 16776582 (0xfffd86) *)
+ := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~0~0~0~1~1~0).
+Notation "'0b111111111111111010001010'" (* 16776842 (0xfffe8a) *)
+ := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~1~0~1~0).
Notation "'0b111111111111111011111111'" (* 16776959 (0xfffeff) *)
:= (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1).
Notation "'0b111111111111111100010110'" (* 16776982 (0xffff16) *)
@@ -1314,6 +1389,8 @@ Notation "'0b111111111111111111001010'" (* 16777162 (0xffffca) *)
:= (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~0).
Notation "'0b111111111111111111011110'" (* 16777182 (0xffffde) *)
:= (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
+Notation "'0b111111111111111111100001'" (* 16777185 (0xffffe1) *)
+ := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1).
Notation "'0b111111111111111111100010'" (* 16777186 (0xffffe2) *)
:= (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0).
Notation "'0b111111111111111111100011'" (* 16777187 (0xffffe3) *)
@@ -1362,10 +1439,14 @@ Notation "'0b1111111111111010111111110'" (* 33551870 (0x1fff5fe) *)
:= (Const WO~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~0).
Notation "'0b1111111111111111010000110'" (* 33554054 (0x1fffe86) *)
:= (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~0~1~0~0~0~0~1~1~0).
+Notation "'0b1111111111111111010001010'" (* 33554058 (0x1fffe8a) *)
+ := (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~0~1~0~0~0~1~0~1~0).
Notation "'0b1111111111111111100101110'" (* 33554222 (0x1ffff2e) *)
:= (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~0~0~1~0~1~1~1~0).
Notation "'0b1111111111111111110001011'" (* 33554315 (0x1ffff8b) *)
:= (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~0~0~0~1~0~1~1).
+Notation "'0b1111111111111111111000010'" (* 33554370 (0x1ffffc2) *)
+ := (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~0~0~0~1~0).
Notation "'0b1111111111111111111000110'" (* 33554374 (0x1ffffc6) *)
:= (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~0~0~1~1~0).
Notation "'0b1111111111111111111001010'" (* 33554378 (0x1ffffca) *)
@@ -1378,12 +1459,16 @@ Notation "'0b1111111111111111111011110'" (* 33554398 (0x1ffffde) *)
:= (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~0).
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 "'0b1111111111111111111100001'" (* 33554401 (0x1ffffe1) *)
+ := (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~0~0~0~1).
Notation "'0b1111111111111111111100010'" (* 33554402 (0x1ffffe2) *)
:= (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~0~0~1~0).
Notation "'0b1111111111111111111100111'" (* 33554407 (0x1ffffe7) *)
:= (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~0~1~1~1).
Notation "'0b1111111111111111111101010'" (* 33554410 (0x1ffffea) *)
:= (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~0~1~0).
+Notation "'0b1111111111111111111101011'" (* 33554411 (0x1ffffeb) *)
+ := (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~0~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 "'0b1111111111111111111101110'" (* 33554414 (0x1ffffee) *)
@@ -1400,6 +1485,8 @@ Notation "'0b1111111111111111111111010'" (* 33554426 (0x1fffffa) *)
:= (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~0~1~0).
Notation "'0b1111111111111111111111011'" (* 33554427 (0x1fffffb) *)
:= (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~0~1~1).
+Notation "'0b1111111111111111111111100'" (* 33554428 (0x1fffffc) *)
+ := (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~0~0).
Notation "'0b1111111111111111111111101'" (* 33554429 (0x1fffffd) *)
:= (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~0~1).
Notation "'0b1111111111111111111111110'" (* 33554430 (0x1fffffe) *)
@@ -1418,8 +1505,12 @@ 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 "'0b11111111111111111111000010'" (* 67108802 (0x3ffffc2) *)
+ := (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~0~0~0~1~0).
Notation "'0b11111111111111111111001110'" (* 67108814 (0x3ffffce) *)
:= (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~0~1~1~1~0).
+Notation "'0b11111111111111111111010110'" (* 67108822 (0x3ffffd6) *)
+ := (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~0~1~1~0).
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 "'0b11111111111111111111011110'" (* 67108830 (0x3ffffde) *)
@@ -1432,6 +1523,8 @@ Notation "'0b11111111111111111111100101'" (* 67108837 (0x3ffffe5) *)
:= (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~0~0~1~0~1).
Notation "'0b11111111111111111111100111'" (* 67108839 (0x3ffffe7) *)
:= (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~0~0~1~1~1).
+Notation "'0b11111111111111111111101011'" (* 67108843 (0x3ffffeb) *)
+ := (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~0~1~0~1~1).
Notation "'0b11111111111111111111101101'" (* 67108845 (0x3ffffed) *)
:= (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~0~1~1~0~1).
Notation "'0b11111111111111111111101110'" (* 67108846 (0x3ffffee) *)
@@ -1448,6 +1541,8 @@ Notation "'0b11111111111111111111111010'" (* 67108858 (0x3fffffa) *)
:= (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~0~1~0).
Notation "'0b11111111111111111111111011'" (* 67108859 (0x3fffffb) *)
:= (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~0~1~1).
+Notation "'0b11111111111111111111111100'" (* 67108860 (0x3fffffc) *)
+ := (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~0~0).
Notation "'0b11111111111111111111111101'" (* 67108861 (0x3fffffd) *)
:= (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~0~1).
Notation "'0b11111111111111111111111110'" (* 67108862 (0x3fffffe) *)
@@ -1468,6 +1563,8 @@ Notation "'0b111111111111111111111001010'" (* 134217674 (0x7ffffca) *)
:= (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~1~0~1~0).
Notation "'0b111111111111111111111001110'" (* 134217678 (0x7ffffce) *)
:= (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~1~1~1~0).
+Notation "'0b111111111111111111111010110'" (* 134217686 (0x7ffffd6) *)
+ := (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~0~1~1~0).
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 "'0b111111111111111111111011110'" (* 134217694 (0x7ffffde) *)
@@ -1484,6 +1581,8 @@ Notation "'0b111111111111111111111101101'" (* 134217709 (0x7ffffed) *)
:= (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~0~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 "'0b111111111111111111111101111'" (* 134217711 (0x7ffffef) *)
+ := (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~1).
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 "'0b111111111111111111111110110'" (* 134217718 (0x7fffff6) *)
@@ -1514,6 +1613,8 @@ Notation "'0b1111111111111111111111001110'" (* 268435406 (0xfffffce) *)
:= (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~0~0~1~1~1~0).
Notation "'0b1111111111111111111111011010'" (* 268435418 (0xfffffda) *)
:= (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~0~1~1~0~1~0).
+Notation "'0b1111111111111111111111011110'" (* 268435422 (0xfffffde) *)
+ := (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~0~1~1~1~1~0).
Notation "'0b1111111111111111111111100010'" (* 268435426 (0xfffffe2) *)
:= (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~0~0~0~1~0).
Notation "'0b1111111111111111111111101110'" (* 268435438 (0xfffffee) *)
@@ -1768,6 +1869,8 @@ Notation "'0b1000000000000000000000000000000000000'" (* 68719476736 (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~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).
Notation "'0b1000000000000000000000000000000000001'" (* 68719476737 (0x1000000001) *)
:= (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~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~1).
+Notation "'0b1111011111111111111111111110000101111'" (* 133143985199 (0x1efffffc2f) *)
+ := (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~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1).
Notation "'0b1111111111111111000000000000000000000'" (* 137436856320 (0x1fffe00000) *)
:= (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~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).
Notation "'0b1111111111111111111111111111000011111'" (* 137438952991 (0x1ffffffe1f) *)
@@ -1778,14 +1881,20 @@ Notation "'0b1111111111111111111111111111110001011'" (* 137438953355 (0x1fffffff
:= (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~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111101110'" (* 137438953454 (0x1fffffffee) *)
:= (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~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111110'" (* 137438953470 (0x1ffffffffe) *)
+ := (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~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111'" (* 137438953471 (0x1fffffffff) *)
:= (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~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0b10000000000000000000000000000000000000'" (* 137438953472 (0x2000000000) *)
:= (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~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).
Notation "'0b10000000000000000000000000000000000001'" (* 137438953473 (0x2000000001) *)
:= (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~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~1).
+Notation "'0b11110111111111111111111111100001011110'" (* 266287970398 (0x3dfffff85e) *)
+ := (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~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1~0).
Notation "'0b11111111111101111111111111111111111111'" (* 274844352511 (0x3ffdffffff) *)
:= (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~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 "'0b11111111111111111111111110111111111111'" (* 274877902847 (0x3fffffefff) *)
+ := (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~1~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).
Notation "'0b11111111111111111111111111111111100111'" (* 274877906919 (0x3fffffffe7) *)
:= (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~1~1~1~1~1~1~1~1~1~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 "'0b11111111111111111111111111111111101111'" (* 274877906927 (0x3fffffffef) *)
@@ -1806,6 +1915,8 @@ Notation "'0b100000000000000000000000000000000000001'" (* 274877906945 (0x400000
:= (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~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~1).
Notation "'0b111111111111011111111111111111111111110'" (* 549688705022 (0x7ffbfffffe) *)
:= (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~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~0).
+Notation "'0b111111111111111111110000000000000000000'" (* 549755289600 (0x7ffff80000) *)
+ := (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~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).
Notation "'0b111111111111111111111111111111110010111'" (* 549755813783 (0x7fffffff97) *)
:= (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~1~1~1~1~1~1~1~1~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 "'0b111111111111111111111111111111111001110'" (* 549755813838 (0x7fffffffce) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index ca63670ff..3727cd1d8 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -42,6 +42,7 @@ nums = tuple(sorted(set(systematic_nums + [
262142,
523807,
524101,
+ 524223,
524262,
524263,
524267,
@@ -51,9 +52,14 @@ nums = tuple(sorted(set(systematic_nums + [
524279,
524286,
679935,
+ 1032192,
+ 1044479,
+ 1047599,
1047811,
1048202,
+ 1048446,
1048471,
+ 1048511,
1048526,
1048534,
1048538,
@@ -65,8 +71,11 @@ nums = tuple(sorted(set(systematic_nums + [
1048574,
1359870,
2060031,
+ 2064384,
2081439,
+ 2088958,
2094335,
+ 2095198,
2095622,
2096127,
2096128,
@@ -85,8 +94,10 @@ nums = tuple(sorted(set(systematic_nums + [
4193327,
4193539,
4193735,
+ 4193883,
4193987,
4194115,
+ 4194240,
4194254,
4194270,
4194271,
@@ -101,11 +112,16 @@ nums = tuple(sorted(set(systematic_nums + [
4194301,
4194302,
8323583,
+ 8372224,
8386654,
8387078,
8387470,
+ 8387766,
8387974,
+ 8388187,
8388230,
+ 8388291,
+ 8388421,
8388491,
8388503,
8388542,
@@ -129,6 +145,9 @@ nums = tuple(sorted(set(systematic_nums + [
16647166,
16711679,
16775935,
+ 16776374,
+ 16776582,
+ 16776842,
16776959,
16776982,
16777006,
@@ -137,6 +156,7 @@ nums = tuple(sorted(set(systematic_nums + [
16777111,
16777162,
16777182,
+ 16777185,
16777186,
16777187,
16777189,
@@ -158,17 +178,21 @@ nums = tuple(sorted(set(systematic_nums + [
33423358,
33551870,
33554054,
+ 33554058,
33554222,
33554315,
+ 33554370,
33554374,
33554378,
33554382,
33554394,
33554398,
33554399,
+ 33554401,
33554402,
33554407,
33554410,
+ 33554411,
33554413,
33554414,
33554415,
@@ -177,19 +201,23 @@ nums = tuple(sorted(set(systematic_nums + [
33554423,
33554426,
33554427,
+ 33554428,
33554429,
33554430,
67107887,
67108630,
67108798,
67108799,
+ 67108802,
67108814,
+ 67108822,
67108826,
67108830,
67108833,
67108834,
67108837,
67108839,
+ 67108843,
67108845,
67108846,
67108847,
@@ -198,6 +226,7 @@ nums = tuple(sorted(set(systematic_nums + [
67108855,
67108858,
67108859,
+ 67108860,
67108861,
67108862,
134215774,
@@ -205,6 +234,7 @@ nums = tuple(sorted(set(systematic_nums + [
134217666,
134217674,
134217678,
+ 134217686,
134217690,
134217694,
134217697,
@@ -213,6 +243,7 @@ nums = tuple(sorted(set(systematic_nums + [
134217703,
134217709,
134217710,
+ 134217711,
134217713,
134217718,
134217719,
@@ -225,6 +256,7 @@ nums = tuple(sorted(set(systematic_nums + [
268435398,
268435406,
268435418,
+ 268435422,
268435426,
268435438,
268435441,
@@ -326,12 +358,16 @@ nums = tuple(sorted(set(systematic_nums + [
68719476727,
68719476733,
68719476734,
+ 133143985199,
137436856320,
137438952991,
137438953285,
137438953355,
137438953454,
+ 137438953470,
+ 266287970398,
274844352511,
+ 274877902847,
274877906919,
274877906927,
274877906933,
@@ -339,6 +375,7 @@ nums = tuple(sorted(set(systematic_nums + [
274877906941,
274877906942,
549688705022,
+ 549755289600,
549755813783,
549755813838,
549755813854,
@@ -1474,6 +1511,10 @@ Notation "'0x7ff45'" (* 524101 (0x7ff45) *)
:= (Const 524101%Z).
Notation "'0x7ff45'" (* 524101 (0x7ff45) *)
:= (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~0~1~0~0~0~1~0~1).
+Notation "'0x7ffbf'" (* 524223 (0x7ffbf) *)
+ := (Const 524223%Z).
+Notation "'0x7ffbf'" (* 524223 (0x7ffbf) *)
+ := (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~0~1~1~1~1~1~1).
Notation "'0x7ffe6'" (* 524262 (0x7ffe6) *)
:= (Const 524262%Z).
Notation "'0x7ffe6'" (* 524262 (0x7ffe6) *)
@@ -1522,6 +1563,18 @@ Notation "'0xa5fff'" (* 679935 (0xa5fff) *)
:= (Const 679935%Z).
Notation "'0xa5fff'" (* 679935 (0xa5fff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0xfc000'" (* 1032192 (0xfc000) *)
+ := (Const 1032192%Z).
+Notation "'0xfc000'" (* 1032192 (0xfc000) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
+Notation "'0xfefff'" (* 1044479 (0xfefff) *)
+ := (Const 1044479%Z).
+Notation "'0xfefff'" (* 1044479 (0xfefff) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0xffc2f'" (* 1047599 (0xffc2f) *)
+ := (Const 1047599%Z).
+Notation "'0xffc2f'" (* 1047599 (0xffc2f) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1).
Notation "'0xffd03'" (* 1047811 (0xffd03) *)
:= (Const 1047811%Z).
Notation "'0xffd03'" (* 1047811 (0xffd03) *)
@@ -1530,10 +1583,18 @@ Notation "'0xffe8a'" (* 1048202 (0xffe8a) *)
:= (Const 1048202%Z).
Notation "'0xffe8a'" (* 1048202 (0xffe8a) *)
:= (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~0~1~0~0~0~1~0~1~0).
+Notation "'0xfff7e'" (* 1048446 (0xfff7e) *)
+ := (Const 1048446%Z).
+Notation "'0xfff7e'" (* 1048446 (0xfff7e) *)
+ := (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~0~1~1~1~1~1~1~0).
Notation "'0xfff97'" (* 1048471 (0xfff97) *)
:= (Const 1048471%Z).
Notation "'0xfff97'" (* 1048471 (0xfff97) *)
:= (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~0~0~1~0~1~1~1).
+Notation "'0xfffbf'" (* 1048511 (0xfffbf) *)
+ := (Const 1048511%Z).
+Notation "'0xfffbf'" (* 1048511 (0xfffbf) *)
+ := (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~0~1~1~1~1~1~1).
Notation "'0xfffce'" (* 1048526 (0xfffce) *)
:= (Const 1048526%Z).
Notation "'0xfffce'" (* 1048526 (0xfffce) *)
@@ -1590,14 +1651,26 @@ Notation "'0x1f6eff'" (* 2060031 (0x1f6eff) *)
:= (Const 2060031%Z).
Notation "'0x1f6eff'" (* 2060031 (0x1f6eff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~0~1~1~0~1~1~1~0~1~1~1~1~1~1~1~1).
+Notation "'0x1f8000'" (* 2064384 (0x1f8000) *)
+ := (Const 2064384%Z).
+Notation "'0x1f8000'" (* 2064384 (0x1f8000) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
Notation "'0x1fc29f'" (* 2081439 (0x1fc29f) *)
:= (Const 2081439%Z).
Notation "'0x1fc29f'" (* 2081439 (0x1fc29f) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~0~0~0~1~0~1~0~0~1~1~1~1~1).
+Notation "'0x1fdffe'" (* 2088958 (0x1fdffe) *)
+ := (Const 2088958%Z).
+Notation "'0x1fdffe'" (* 2088958 (0x1fdffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0x1ff4ff'" (* 2094335 (0x1ff4ff) *)
:= (Const 2094335%Z).
Notation "'0x1ff4ff'" (* 2094335 (0x1ff4ff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~0~1~0~0~1~1~1~1~1~1~1~1).
+Notation "'0x1ff85e'" (* 2095198 (0x1ff85e) *)
+ := (Const 2095198%Z).
+Notation "'0x1ff85e'" (* 2095198 (0x1ff85e) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1~0).
Notation "'0x1ffa06'" (* 2095622 (0x1ffa06) *)
:= (Const 2095622%Z).
Notation "'0x1ffa06'" (* 2095622 (0x1ffa06) *)
@@ -1682,6 +1755,10 @@ Notation "'0x3ffdc7'" (* 4193735 (0x3ffdc7) *)
:= (Const 4193735%Z).
Notation "'0x3ffdc7'" (* 4193735 (0x3ffdc7) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1).
+Notation "'0x3ffe5b'" (* 4193883 (0x3ffe5b) *)
+ := (Const 4193883%Z).
+Notation "'0x3ffe5b'" (* 4193883 (0x3ffe5b) *)
+ := (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~0~0~1~0~1~1~0~1~1).
Notation "'0x3ffec3'" (* 4193987 (0x3ffec3) *)
:= (Const 4193987%Z).
Notation "'0x3ffec3'" (* 4193987 (0x3ffec3) *)
@@ -1690,6 +1767,10 @@ Notation "'0x3fff43'" (* 4194115 (0x3fff43) *)
:= (Const 4194115%Z).
Notation "'0x3fff43'" (* 4194115 (0x3fff43) *)
:= (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~0~1~0~0~0~0~1~1).
+Notation "'0x3fffc0'" (* 4194240 (0x3fffc0) *)
+ := (Const 4194240%Z).
+Notation "'0x3fffc0'" (* 4194240 (0x3fffc0) *)
+ := (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~0~0~0~0~0~0).
Notation "'0x3fffce'" (* 4194254 (0x3fffce) *)
:= (Const 4194254%Z).
Notation "'0x3fffce'" (* 4194254 (0x3fffce) *)
@@ -1758,6 +1839,10 @@ Notation "'0x7f01ff'" (* 8323583 (0x7f01ff) *)
:= (Const 8323583%Z).
Notation "'0x7f01ff'" (* 8323583 (0x7f01ff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1).
+Notation "'0x7fc000'" (* 8372224 (0x7fc000) *)
+ := (Const 8372224%Z).
+Notation "'0x7fc000'" (* 8372224 (0x7fc000) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
Notation "'0x7ff85e'" (* 8386654 (0x7ff85e) *)
:= (Const 8386654%Z).
Notation "'0x7ff85e'" (* 8386654 (0x7ff85e) *)
@@ -1770,14 +1855,30 @@ Notation "'0x7ffb8e'" (* 8387470 (0x7ffb8e) *)
:= (Const 8387470%Z).
Notation "'0x7ffb8e'" (* 8387470 (0x7ffb8e) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1~0).
+Notation "'0x7ffcb6'" (* 8387766 (0x7ffcb6) *)
+ := (Const 8387766%Z).
+Notation "'0x7ffcb6'" (* 8387766 (0x7ffcb6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~0~1~1~0).
Notation "'0x7ffd86'" (* 8387974 (0x7ffd86) *)
:= (Const 8387974%Z).
Notation "'0x7ffd86'" (* 8387974 (0x7ffd86) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~0~0~0~1~1~0).
+Notation "'0x7ffe5b'" (* 8388187 (0x7ffe5b) *)
+ := (Const 8388187%Z).
+Notation "'0x7ffe5b'" (* 8388187 (0x7ffe5b) *)
+ := (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~0~0~1~0~1~1~0~1~1).
Notation "'0x7ffe86'" (* 8388230 (0x7ffe86) *)
:= (Const 8388230%Z).
Notation "'0x7ffe86'" (* 8388230 (0x7ffe86) *)
:= (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~0~1~0~0~0~0~1~1~0).
+Notation "'0x7ffec3'" (* 8388291 (0x7ffec3) *)
+ := (Const 8388291%Z).
+Notation "'0x7ffec3'" (* 8388291 (0x7ffec3) *)
+ := (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~0~1~1~0~0~0~0~1~1).
+Notation "'0x7fff45'" (* 8388421 (0x7fff45) *)
+ := (Const 8388421%Z).
+Notation "'0x7fff45'" (* 8388421 (0x7fff45) *)
+ := (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~0~1~0~0~0~1~0~1).
Notation "'0x7fff8b'" (* 8388491 (0x7fff8b) *)
:= (Const 8388491%Z).
Notation "'0x7fff8b'" (* 8388491 (0x7fff8b) *)
@@ -1882,6 +1983,18 @@ Notation "'0xfffaff'" (* 16775935 (0xfffaff) *)
:= (Const 16775935%Z).
Notation "'0xfffaff'" (* 16775935 (0xfffaff) *)
:= (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1~1~1~1~1~1~1).
+Notation "'0xfffcb6'" (* 16776374 (0xfffcb6) *)
+ := (Const 16776374%Z).
+Notation "'0xfffcb6'" (* 16776374 (0xfffcb6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~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 "'0xfffd86'" (* 16776582 (0xfffd86) *)
+ := (Const 16776582%Z).
+Notation "'0xfffd86'" (* 16776582 (0xfffd86) *)
+ := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~0~0~0~1~1~0).
+Notation "'0xfffe8a'" (* 16776842 (0xfffe8a) *)
+ := (Const 16776842%Z).
+Notation "'0xfffe8a'" (* 16776842 (0xfffe8a) *)
+ := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~1~0~1~0).
Notation "'0xfffeff'" (* 16776959 (0xfffeff) *)
:= (Const 16776959%Z).
Notation "'0xfffeff'" (* 16776959 (0xfffeff) *)
@@ -1914,6 +2027,10 @@ Notation "'0xffffde'" (* 16777182 (0xffffde) *)
:= (Const 16777182%Z).
Notation "'0xffffde'" (* 16777182 (0xffffde) *)
:= (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
+Notation "'0xffffe1'" (* 16777185 (0xffffe1) *)
+ := (Const 16777185%Z).
+Notation "'0xffffe1'" (* 16777185 (0xffffe1) *)
+ := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1).
Notation "'0xffffe2'" (* 16777186 (0xffffe2) *)
:= (Const 16777186%Z).
Notation "'0xffffe2'" (* 16777186 (0xffffe2) *)
@@ -2010,6 +2127,10 @@ Notation "'0x1fffe86'" (* 33554054 (0x1fffe86) *)
:= (Const 33554054%Z).
Notation "'0x1fffe86'" (* 33554054 (0x1fffe86) *)
:= (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~0~1~0~0~0~0~1~1~0).
+Notation "'0x1fffe8a'" (* 33554058 (0x1fffe8a) *)
+ := (Const 33554058%Z).
+Notation "'0x1fffe8a'" (* 33554058 (0x1fffe8a) *)
+ := (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~0~1~0~0~0~1~0~1~0).
Notation "'0x1ffff2e'" (* 33554222 (0x1ffff2e) *)
:= (Const 33554222%Z).
Notation "'0x1ffff2e'" (* 33554222 (0x1ffff2e) *)
@@ -2018,6 +2139,10 @@ Notation "'0x1ffff8b'" (* 33554315 (0x1ffff8b) *)
:= (Const 33554315%Z).
Notation "'0x1ffff8b'" (* 33554315 (0x1ffff8b) *)
:= (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~0~0~0~1~0~1~1).
+Notation "'0x1ffffc2'" (* 33554370 (0x1ffffc2) *)
+ := (Const 33554370%Z).
+Notation "'0x1ffffc2'" (* 33554370 (0x1ffffc2) *)
+ := (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~0~0~0~1~0).
Notation "'0x1ffffc6'" (* 33554374 (0x1ffffc6) *)
:= (Const 33554374%Z).
Notation "'0x1ffffc6'" (* 33554374 (0x1ffffc6) *)
@@ -2042,6 +2167,10 @@ 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 "'0x1ffffe1'" (* 33554401 (0x1ffffe1) *)
+ := (Const 33554401%Z).
+Notation "'0x1ffffe1'" (* 33554401 (0x1ffffe1) *)
+ := (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~0~0~0~1).
Notation "'0x1ffffe2'" (* 33554402 (0x1ffffe2) *)
:= (Const 33554402%Z).
Notation "'0x1ffffe2'" (* 33554402 (0x1ffffe2) *)
@@ -2054,6 +2183,10 @@ Notation "'0x1ffffea'" (* 33554410 (0x1ffffea) *)
:= (Const 33554410%Z).
Notation "'0x1ffffea'" (* 33554410 (0x1ffffea) *)
:= (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~0~1~0).
+Notation "'0x1ffffeb'" (* 33554411 (0x1ffffeb) *)
+ := (Const 33554411%Z).
+Notation "'0x1ffffeb'" (* 33554411 (0x1ffffeb) *)
+ := (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~0~1~1).
Notation "'0x1ffffed'" (* 33554413 (0x1ffffed) *)
:= (Const 33554413%Z).
Notation "'0x1ffffed'" (* 33554413 (0x1ffffed) *)
@@ -2086,6 +2219,10 @@ Notation "'0x1fffffb'" (* 33554427 (0x1fffffb) *)
:= (Const 33554427%Z).
Notation "'0x1fffffb'" (* 33554427 (0x1fffffb) *)
:= (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~0~1~1).
+Notation "'0x1fffffc'" (* 33554428 (0x1fffffc) *)
+ := (Const 33554428%Z).
+Notation "'0x1fffffc'" (* 33554428 (0x1fffffc) *)
+ := (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~0~0).
Notation "'0x1fffffd'" (* 33554429 (0x1fffffd) *)
:= (Const 33554429%Z).
Notation "'0x1fffffd'" (* 33554429 (0x1fffffd) *)
@@ -2122,10 +2259,18 @@ 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 "'0x3ffffc2'" (* 67108802 (0x3ffffc2) *)
+ := (Const 67108802%Z).
+Notation "'0x3ffffc2'" (* 67108802 (0x3ffffc2) *)
+ := (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~0~0~0~1~0).
Notation "'0x3ffffce'" (* 67108814 (0x3ffffce) *)
:= (Const 67108814%Z).
Notation "'0x3ffffce'" (* 67108814 (0x3ffffce) *)
:= (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~0~1~1~1~0).
+Notation "'0x3ffffd6'" (* 67108822 (0x3ffffd6) *)
+ := (Const 67108822%Z).
+Notation "'0x3ffffd6'" (* 67108822 (0x3ffffd6) *)
+ := (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~0~1~1~0).
Notation "'0x3ffffda'" (* 67108826 (0x3ffffda) *)
:= (Const 67108826%Z).
Notation "'0x3ffffda'" (* 67108826 (0x3ffffda) *)
@@ -2150,6 +2295,10 @@ Notation "'0x3ffffe7'" (* 67108839 (0x3ffffe7) *)
:= (Const 67108839%Z).
Notation "'0x3ffffe7'" (* 67108839 (0x3ffffe7) *)
:= (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~0~0~1~1~1).
+Notation "'0x3ffffeb'" (* 67108843 (0x3ffffeb) *)
+ := (Const 67108843%Z).
+Notation "'0x3ffffeb'" (* 67108843 (0x3ffffeb) *)
+ := (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~0~1~0~1~1).
Notation "'0x3ffffed'" (* 67108845 (0x3ffffed) *)
:= (Const 67108845%Z).
Notation "'0x3ffffed'" (* 67108845 (0x3ffffed) *)
@@ -2182,6 +2331,10 @@ Notation "'0x3fffffb'" (* 67108859 (0x3fffffb) *)
:= (Const 67108859%Z).
Notation "'0x3fffffb'" (* 67108859 (0x3fffffb) *)
:= (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~0~1~1).
+Notation "'0x3fffffc'" (* 67108860 (0x3fffffc) *)
+ := (Const 67108860%Z).
+Notation "'0x3fffffc'" (* 67108860 (0x3fffffc) *)
+ := (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~0~0).
Notation "'0x3fffffd'" (* 67108861 (0x3fffffd) *)
:= (Const 67108861%Z).
Notation "'0x3fffffd'" (* 67108861 (0x3fffffd) *)
@@ -2222,6 +2375,10 @@ Notation "'0x7ffffce'" (* 134217678 (0x7ffffce) *)
:= (Const 134217678%Z).
Notation "'0x7ffffce'" (* 134217678 (0x7ffffce) *)
:= (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~1~1~1~0).
+Notation "'0x7ffffd6'" (* 134217686 (0x7ffffd6) *)
+ := (Const 134217686%Z).
+Notation "'0x7ffffd6'" (* 134217686 (0x7ffffd6) *)
+ := (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~0~1~1~0).
Notation "'0x7ffffda'" (* 134217690 (0x7ffffda) *)
:= (Const 134217690%Z).
Notation "'0x7ffffda'" (* 134217690 (0x7ffffda) *)
@@ -2254,6 +2411,10 @@ Notation "'0x7ffffee'" (* 134217710 (0x7ffffee) *)
:= (Const 134217710%Z).
Notation "'0x7ffffee'" (* 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 "'0x7ffffef'" (* 134217711 (0x7ffffef) *)
+ := (Const 134217711%Z).
+Notation "'0x7ffffef'" (* 134217711 (0x7ffffef) *)
+ := (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~1).
Notation "'0x7fffff1'" (* 134217713 (0x7fffff1) *)
:= (Const 134217713%Z).
Notation "'0x7fffff1'" (* 134217713 (0x7fffff1) *)
@@ -2314,6 +2475,10 @@ Notation "'0xfffffda'" (* 268435418 (0xfffffda) *)
:= (Const 268435418%Z).
Notation "'0xfffffda'" (* 268435418 (0xfffffda) *)
:= (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~0~1~1~0~1~0).
+Notation "'0xfffffde'" (* 268435422 (0xfffffde) *)
+ := (Const 268435422%Z).
+Notation "'0xfffffde'" (* 268435422 (0xfffffde) *)
+ := (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~0~1~1~1~1~0).
Notation "'0xfffffe2'" (* 268435426 (0xfffffe2) *)
:= (Const 268435426%Z).
Notation "'0xfffffe2'" (* 268435426 (0xfffffe2) *)
@@ -2822,6 +2987,10 @@ Notation "'0x1000000001'" (* 68719476737 (0x1000000001) *)
:= (Const 68719476737%Z).
Notation "'0x1000000001'" (* 68719476737 (0x1000000001) *)
:= (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~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~1).
+Notation "'0x1efffffc2f'" (* 133143985199 (0x1efffffc2f) *)
+ := (Const 133143985199%Z).
+Notation "'0x1efffffc2f'" (* 133143985199 (0x1efffffc2f) *)
+ := (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~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1).
Notation "'0x1fffe00000'" (* 137436856320 (0x1fffe00000) *)
:= (Const 137436856320%Z).
Notation "'0x1fffe00000'" (* 137436856320 (0x1fffe00000) *)
@@ -2842,6 +3011,10 @@ Notation "'0x1fffffffee'" (* 137438953454 (0x1fffffffee) *)
:= (Const 137438953454%Z).
Notation "'0x1fffffffee'" (* 137438953454 (0x1fffffffee) *)
:= (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~1~1~1~1~1~1~1~1~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 "'0x1ffffffffe'" (* 137438953470 (0x1ffffffffe) *)
+ := (Const 137438953470%Z).
+Notation "'0x1ffffffffe'" (* 137438953470 (0x1ffffffffe) *)
+ := (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~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0x1fffffffff'" (* 137438953471 (0x1fffffffff) *)
:= (Const 137438953471%Z).
Notation "'0x1fffffffff'" (* 137438953471 (0x1fffffffff) *)
@@ -2854,10 +3027,18 @@ Notation "'0x2000000001'" (* 137438953473 (0x2000000001) *)
:= (Const 137438953473%Z).
Notation "'0x2000000001'" (* 137438953473 (0x2000000001) *)
:= (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~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~1).
+Notation "'0x3dfffff85e'" (* 266287970398 (0x3dfffff85e) *)
+ := (Const 266287970398%Z).
+Notation "'0x3dfffff85e'" (* 266287970398 (0x3dfffff85e) *)
+ := (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~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1~0).
Notation "'0x3ffdffffff'" (* 274844352511 (0x3ffdffffff) *)
:= (Const 274844352511%Z).
Notation "'0x3ffdffffff'" (* 274844352511 (0x3ffdffffff) *)
:= (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~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 "'0x3fffffefff'" (* 274877902847 (0x3fffffefff) *)
+ := (Const 274877902847%Z).
+Notation "'0x3fffffefff'" (* 274877902847 (0x3fffffefff) *)
+ := (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~1~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).
Notation "'0x3fffffffe7'" (* 274877906919 (0x3fffffffe7) *)
:= (Const 274877906919%Z).
Notation "'0x3fffffffe7'" (* 274877906919 (0x3fffffffe7) *)
@@ -2898,6 +3079,10 @@ Notation "'0x7ffbfffffe'" (* 549688705022 (0x7ffbfffffe) *)
:= (Const 549688705022%Z).
Notation "'0x7ffbfffffe'" (* 549688705022 (0x7ffbfffffe) *)
:= (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~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~0).
+Notation "'0x7ffff80000'" (* 549755289600 (0x7ffff80000) *)
+ := (Const 549755289600%Z).
+Notation "'0x7ffff80000'" (* 549755289600 (0x7ffff80000) *)
+ := (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~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).
Notation "'0x7fffffff97'" (* 549755813783 (0x7fffffff97) *)
:= (Const 549755813783%Z).
Notation "'0x7fffffff97'" (* 549755813783 (0x7fffffff97) *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 03:14:16 +0000