aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-11-02 12:45:09 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-11-02 12:45:09 -0400
commit3a5c4795e1a0f7d4b8803022ac9f28e1bc8c031d (patch)
tree50dd745f834649f9fa287a82f474577b038e1ccb /src/Compilers
parent228495914cf66eac4c0512d547a70b1ed40c56d0 (diff)
Add more constant notations
Diffstat (limited to 'src/Compilers')
-rw-r--r--src/Compilers/Z/BinaryNotationConstants.v57
-rw-r--r--src/Compilers/Z/HexNotationConstants.v95
2 files changed, 152 insertions, 0 deletions
diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index e5e816862..82f6b76a3 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -34,8 +34,10 @@ nums = tuple(sorted(set(systematic_nums + [
261575,
262131,
262139,
+ 262142,
523807,
524101,
+ 524262,
524263,
524267,
524269,
@@ -86,6 +88,7 @@ nums = tuple(sorted(set(systematic_nums + [
16777207,
16777213,
16777214,
+ 33423358,
33554378,
33554399,
33554413,
@@ -94,6 +97,7 @@ nums = tuple(sorted(set(systematic_nums + [
33554427,
33554429,
33554430,
+ 67108798,
67108833,
67108845,
67108847,
@@ -114,10 +118,12 @@ nums = tuple(sorted(set(systematic_nums + [
134217719,
134217726,
268431360,
+ 268435398,
268435406,
268435426,
268435441,
268435445,
+ 268435452,
268435453,
268435454,
536870882,
@@ -132,6 +138,7 @@ nums = tuple(sorted(set(systematic_nums + [
1054736383,
1065418751,
1073709055,
+ 1073741814,
1073741818,
1073741821,
1073741822,
@@ -247,6 +254,7 @@ nums = tuple(sorted(set(systematic_nums + [
281470681743359,
281474976645119,
281474976710339,
+ 281474976710606,
281474976710626,
281474976710631,
281474976710638,
@@ -255,7 +263,10 @@ nums = tuple(sorted(set(systematic_nums + [
281474976710647,
281474976710653,
281474976710654,
+ 389227116232702,
+ 562907003748350,
562949953290238,
+ 562949953420678,
562949953421262,
562949953421279,
562949953421290,
@@ -292,6 +303,7 @@ nums = tuple(sorted(set(systematic_nums + [
4503599627370015,
4503599627370307,
4503599627370309,
+ 4503599627370434,
4503599627370458,
4503599627370478,
4503599627370479,
@@ -302,6 +314,7 @@ nums = tuple(sorted(set(systematic_nums + [
9007199254740614,
9007199254740963,
9007199254740982,
+ 9007199254740988,
9007199254740990,
18014398509481926,
18014398509481975,
@@ -331,6 +344,7 @@ nums = tuple(sorted(set(systematic_nums + [
144115188075855863,
144115188075855866,
144115188075855867,
+ 144115188075855868,
144115188075855869,
144115188075855870,
288230376151711706,
@@ -339,6 +353,8 @@ nums = tuple(sorted(set(systematic_nums + [
288230376151711726,
288230376151711727,
288230376151711734,
+ 288230376151711738,
+ 288230376151711740,
288230376151711741,
288230376151711742,
576460752303423434,
@@ -351,7 +367,10 @@ nums = tuple(sorted(set(systematic_nums + [
1117984489315730401,
1152921504606846934,
1152921504606846938,
+ 1152921504606846942,
1152921504606846974,
+ 2305843009213693948,
+ 2305843009213693950,
3353953467947191203,
3816567739388183093,
4530058275181297663,
@@ -816,6 +835,8 @@ Notation "'0b111111111111110011'" (* 262131 (0x3fff3) *)
:= (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~0~0~1~1).
Notation "'0b111111111111111011'" (* 262139 (0x3fffb) *)
:= (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~0~1~1).
+Notation "'0b111111111111111110'" (* 262142 (0x3fffe) *)
+ := (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~0).
Notation "'0b111111111111111111'" (* 262143 (0x3ffff) *)
:= (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).
Notation "'0b1000000000000000000'" (* 262144 (0x40000) *)
@@ -826,6 +847,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 "'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) *)
:= (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~1).
Notation "'0b1111111111111101011'" (* 524267 (0x7ffeb) *)
@@ -962,6 +985,8 @@ Notation "'0b1000000000000000000000000'" (* 16777216 (0x1000000) *)
:= (Const WO~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
Notation "'0b1000000000000000000000001'" (* 16777217 (0x1000001) *)
:= (Const WO~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0b1111111011111111111111110'" (* 33423358 (0x1fdfffe) *)
+ := (Const WO~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~0).
Notation "'0b1111111111111111111001010'" (* 33554378 (0x1ffffca) *)
:= (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~1~0~1~0).
Notation "'0b1111111111111111111011111'" (* 33554399 (0x1ffffdf) *)
@@ -984,6 +1009,8 @@ 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 "'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 "'0b11111111111111111111100001'" (* 67108833 (0x3ffffe1) *)
:= (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~0~0~1).
Notation "'0b11111111111111111111101101'" (* 67108845 (0x3ffffed) *)
@@ -1036,6 +1063,8 @@ Notation "'0b1000000000000000000000000001'" (* 134217729 (0x8000001) *)
:= (Const WO~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
Notation "'0b1111111111111111000000000000'" (* 268431360 (0xffff000) *)
:= (Const WO~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).
+Notation "'0b1111111111111111111111000110'" (* 268435398 (0xfffffc6) *)
+ := (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~0~1~1~0).
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 "'0b1111111111111111111111100010'" (* 268435426 (0xfffffe2) *)
@@ -1044,6 +1073,8 @@ Notation "'0b1111111111111111111111110001'" (* 268435441 (0xffffff1) *)
:= (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~0~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 "'0b1111111111111111111111111100'" (* 268435452 (0xffffffc) *)
+ := (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0).
Notation "'0b1111111111111111111111111101'" (* 268435453 (0xffffffd) *)
:= (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1).
Notation "'0b1111111111111111111111111110'" (* 268435454 (0xffffffe) *)
@@ -1084,6 +1115,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 "'0b111111111111111111111111110110'" (* 1073741814 (0x3ffffff6) *)
+ := (Const WO~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
Notation "'0b111111111111111111111111111010'" (* 1073741818 (0x3ffffffa) *)
:= (Const WO~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
Notation "'0b111111111111111111111111111101'" (* 1073741821 (0x3ffffffd) *)
@@ -1420,6 +1453,8 @@ Notation "'0b111111111111111111111111111111101111111111111111'" (* 2814749766451
:= (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 "'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 "'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 "'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) *)
@@ -1442,8 +1477,14 @@ Notation "'0b1000000000000000000000000000000000000000000000000'" (* 281474976710
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
Notation "'0b1000000000000000000000000000000000000000000000001'" (* 281474976710657 (0x1000000000001) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0b1011000011111111111111111111111111111111111111110'" (* 389227116232702 (0x161fffffffffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~1~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
+Notation "'0b1111111111111010111111111111111111111111111111110'" (* 562907003748350 (0x1fff5fffffffe) *)
+ := (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 "'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 "'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 "'0b1111111111111111111111111111111111111111111011111'" (* 562949953421279 (0x1ffffffffffdf) *)
@@ -1534,6 +1575,8 @@ Notation "'0b1111111111111111111111111111111111111111111101000011'" (* 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~0~1~0~0~0~0~1~1).
Notation "'0b1111111111111111111111111111111111111111111101000101'" (* 4503599627370309 (0xfffffffffff45) *)
:= (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~0~1~0~0~0~1~0~1).
+Notation "'0b1111111111111111111111111111111111111111111111000010'" (* 4503599627370434 (0xfffffffffffc2) *)
+ := (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~0~0~0~1~0).
Notation "'0b1111111111111111111111111111111111111111111111011010'" (* 4503599627370458 (0xfffffffffffda) *)
:= (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 "'0b1111111111111111111111111111111111111111111111101110'" (* 4503599627370478 (0xfffffffffffee) *)
@@ -1560,6 +1603,8 @@ Notation "'0b11111111111111111111111111111111111111111111111100011'" (* 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~1~1~1~1~0~0~0~1~1).
Notation "'0b11111111111111111111111111111111111111111111111110110'" (* 9007199254740982 (0x1ffffffffffff6) *)
:= (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~1~1~0).
+Notation "'0b11111111111111111111111111111111111111111111111111100'" (* 9007199254740988 (0x1ffffffffffffc) *)
+ := (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~1~1~0~0).
Notation "'0b11111111111111111111111111111111111111111111111111110'" (* 9007199254740990 (0x1ffffffffffffe) *)
:= (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~1~1~1~0).
Notation "'0b11111111111111111111111111111111111111111111111111111'" (* 9007199254740991 (0x1fffffffffffff) *)
@@ -1642,6 +1687,8 @@ Notation "'0b111111111111111111111111111111111111111111111111111111010'" (* 1441
:= (Const WO~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
Notation "'0b111111111111111111111111111111111111111111111111111111011'" (* 144115188075855867 (0x1fffffffffffffb) *)
:= (Const WO~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1).
+Notation "'0b111111111111111111111111111111111111111111111111111111100'" (* 144115188075855868 (0x1fffffffffffffc) *)
+ := (Const WO~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0).
Notation "'0b111111111111111111111111111111111111111111111111111111101'" (* 144115188075855869 (0x1fffffffffffffd) *)
:= (Const WO~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1).
Notation "'0b111111111111111111111111111111111111111111111111111111110'" (* 144115188075855870 (0x1fffffffffffffe) *)
@@ -1664,6 +1711,10 @@ Notation "'0b1111111111111111111111111111111111111111111111111111101111'" (* 288
:= (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~1~1~1~1).
Notation "'0b1111111111111111111111111111111111111111111111111111110110'" (* 288230376151711734 (0x3fffffffffffff6) *)
:= (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~1~0~1~1~0).
+Notation "'0b1111111111111111111111111111111111111111111111111111111010'" (* 288230376151711738 (0x3fffffffffffffa) *)
+ := (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~1~1~0~1~0).
+Notation "'0b1111111111111111111111111111111111111111111111111111111100'" (* 288230376151711740 (0x3fffffffffffffc) *)
+ := (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~1~1~1~0~0).
Notation "'0b1111111111111111111111111111111111111111111111111111111101'" (* 288230376151711741 (0x3fffffffffffffd) *)
:= (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~1~1~1~0~1).
Notation "'0b1111111111111111111111111111111111111111111111111111111110'" (* 288230376151711742 (0x3fffffffffffffe) *)
@@ -1700,6 +1751,8 @@ Notation "'0b111111111111111111111111111111111111111111111111111111010110'" (* 1
:= (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1~0).
Notation "'0b111111111111111111111111111111111111111111111111111111011010'" (* 1152921504606846938 (0xfffffffffffffda) *)
:= (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
+Notation "'0b111111111111111111111111111111111111111111111111111111011110'" (* 1152921504606846942 (0xfffffffffffffde) *)
+ := (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
Notation "'0b111111111111111111111111111111111111111111111111111111111110'" (* 1152921504606846974 (0xffffffffffffffe) *)
:= (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0b111111111111111111111111111111111111111111111111111111111111'" (* 1152921504606846975 (0xfffffffffffffff) *)
@@ -1708,6 +1761,10 @@ Notation "'0b1000000000000000000000000000000000000000000000000000000000000'" (*
:= (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~0~0~0~0~0~0~0~0~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 "'0b1000000000000000000000000000000000000000000000000000000000001'" (* 1152921504606846977 (0x1000000000000001) *)
:= (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~0~0~0~0~0~0~0~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 "'0b1111111111111111111111111111111111111111111111111111111111100'" (* 2305843009213693948 (0x1ffffffffffffffc) *)
+ := (Const WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111111111110'" (* 2305843009213693950 (0x1ffffffffffffffe) *)
+ := (Const WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111111111111'" (* 2305843009213693951 (0x1fffffffffffffff) *)
:= (Const WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0b10000000000000000000000000000000000000000000000000000000000000'" (* 2305843009213693952 (0x2000000000000000) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 652d4af06..55878a0cd 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -34,8 +34,10 @@ nums = tuple(sorted(set(systematic_nums + [
261575,
262131,
262139,
+ 262142,
523807,
524101,
+ 524262,
524263,
524267,
524269,
@@ -86,6 +88,7 @@ nums = tuple(sorted(set(systematic_nums + [
16777207,
16777213,
16777214,
+ 33423358,
33554378,
33554399,
33554413,
@@ -94,6 +97,7 @@ nums = tuple(sorted(set(systematic_nums + [
33554427,
33554429,
33554430,
+ 67108798,
67108833,
67108845,
67108847,
@@ -114,10 +118,12 @@ nums = tuple(sorted(set(systematic_nums + [
134217719,
134217726,
268431360,
+ 268435398,
268435406,
268435426,
268435441,
268435445,
+ 268435452,
268435453,
268435454,
536870882,
@@ -132,6 +138,7 @@ nums = tuple(sorted(set(systematic_nums + [
1054736383,
1065418751,
1073709055,
+ 1073741814,
1073741818,
1073741821,
1073741822,
@@ -247,6 +254,7 @@ nums = tuple(sorted(set(systematic_nums + [
281470681743359,
281474976645119,
281474976710339,
+ 281474976710606,
281474976710626,
281474976710631,
281474976710638,
@@ -255,7 +263,10 @@ nums = tuple(sorted(set(systematic_nums + [
281474976710647,
281474976710653,
281474976710654,
+ 389227116232702,
+ 562907003748350,
562949953290238,
+ 562949953420678,
562949953421262,
562949953421279,
562949953421290,
@@ -292,6 +303,7 @@ nums = tuple(sorted(set(systematic_nums + [
4503599627370015,
4503599627370307,
4503599627370309,
+ 4503599627370434,
4503599627370458,
4503599627370478,
4503599627370479,
@@ -302,6 +314,7 @@ nums = tuple(sorted(set(systematic_nums + [
9007199254740614,
9007199254740963,
9007199254740982,
+ 9007199254740988,
9007199254740990,
18014398509481926,
18014398509481975,
@@ -331,6 +344,7 @@ nums = tuple(sorted(set(systematic_nums + [
144115188075855863,
144115188075855866,
144115188075855867,
+ 144115188075855868,
144115188075855869,
144115188075855870,
288230376151711706,
@@ -339,6 +353,8 @@ nums = tuple(sorted(set(systematic_nums + [
288230376151711726,
288230376151711727,
288230376151711734,
+ 288230376151711738,
+ 288230376151711740,
288230376151711741,
288230376151711742,
576460752303423434,
@@ -351,7 +367,10 @@ nums = tuple(sorted(set(systematic_nums + [
1117984489315730401,
1152921504606846934,
1152921504606846938,
+ 1152921504606846942,
1152921504606846974,
+ 2305843009213693948,
+ 2305843009213693950,
3353953467947191203,
3816567739388183093,
4530058275181297663,
@@ -1174,6 +1193,10 @@ Notation "'0x3fffb'" (* 262139 (0x3fffb) *)
:= (Const 262139%Z).
Notation "'0x3fffb'" (* 262139 (0x3fffb) *)
:= (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~0~1~1).
+Notation "'0x3fffe'" (* 262142 (0x3fffe) *)
+ := (Const 262142%Z).
+Notation "'0x3fffe'" (* 262142 (0x3fffe) *)
+ := (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~0).
Notation "'0x3ffff'" (* 262143 (0x3ffff) *)
:= (Const 262143%Z).
Notation "'0x3ffff'" (* 262143 (0x3ffff) *)
@@ -1194,6 +1217,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 "'0x7ffe6'" (* 524262 (0x7ffe6) *)
+ := (Const 524262%Z).
+Notation "'0x7ffe6'" (* 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 "'0x7ffe7'" (* 524263 (0x7ffe7) *)
:= (Const 524263%Z).
Notation "'0x7ffe7'" (* 524263 (0x7ffe7) *)
@@ -1466,6 +1493,10 @@ Notation "'0x1000001'" (* 16777217 (0x1000001) *)
:= (Const 16777217%Z).
Notation "'0x1000001'" (* 16777217 (0x1000001) *)
:= (Const WO~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0x1fdfffe'" (* 33423358 (0x1fdfffe) *)
+ := (Const 33423358%Z).
+Notation "'0x1fdfffe'" (* 33423358 (0x1fdfffe) *)
+ := (Const WO~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~0).
Notation "'0x1ffffca'" (* 33554378 (0x1ffffca) *)
:= (Const 33554378%Z).
Notation "'0x1ffffca'" (* 33554378 (0x1ffffca) *)
@@ -1510,6 +1541,10 @@ 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 "'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 "'0x3ffffe1'" (* 67108833 (0x3ffffe1) *)
:= (Const 67108833%Z).
Notation "'0x3ffffe1'" (* 67108833 (0x3ffffe1) *)
@@ -1614,6 +1649,10 @@ Notation "'0xffff000'" (* 268431360 (0xffff000) *)
:= (Const 268431360%Z).
Notation "'0xffff000'" (* 268431360 (0xffff000) *)
:= (Const WO~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).
+Notation "'0xfffffc6'" (* 268435398 (0xfffffc6) *)
+ := (Const 268435398%Z).
+Notation "'0xfffffc6'" (* 268435398 (0xfffffc6) *)
+ := (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~0~1~1~0).
Notation "'0xfffffce'" (* 268435406 (0xfffffce) *)
:= (Const 268435406%Z).
Notation "'0xfffffce'" (* 268435406 (0xfffffce) *)
@@ -1630,6 +1669,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 "'0xffffffc'" (* 268435452 (0xffffffc) *)
+ := (Const 268435452%Z).
+Notation "'0xffffffc'" (* 268435452 (0xffffffc) *)
+ := (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0).
Notation "'0xffffffd'" (* 268435453 (0xffffffd) *)
:= (Const 268435453%Z).
Notation "'0xffffffd'" (* 268435453 (0xffffffd) *)
@@ -1710,6 +1753,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 "'0x3ffffff6'" (* 1073741814 (0x3ffffff6) *)
+ := (Const 1073741814%Z).
+Notation "'0x3ffffff6'" (* 1073741814 (0x3ffffff6) *)
+ := (Const WO~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
Notation "'0x3ffffffa'" (* 1073741818 (0x3ffffffa) *)
:= (Const 1073741818%Z).
Notation "'0x3ffffffa'" (* 1073741818 (0x3ffffffa) *)
@@ -2382,6 +2429,10 @@ 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 "'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 "'0xffffffffffe2'" (* 281474976710626 (0xffffffffffe2) *)
:= (Const 281474976710626%Z).
Notation "'0xffffffffffe2'" (* 281474976710626 (0xffffffffffe2) *)
@@ -2426,10 +2477,22 @@ Notation "'0x1000000000001'" (* 281474976710657 (0x1000000000001) *)
:= (Const 281474976710657%Z).
Notation "'0x1000000000001'" (* 281474976710657 (0x1000000000001) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0x161fffffffffe'" (* 389227116232702 (0x161fffffffffe) *)
+ := (Const 389227116232702%Z).
+Notation "'0x161fffffffffe'" (* 389227116232702 (0x161fffffffffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~1~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
+Notation "'0x1fff5fffffffe'" (* 562907003748350 (0x1fff5fffffffe) *)
+ := (Const 562907003748350%Z).
+Notation "'0x1fff5fffffffe'" (* 562907003748350 (0x1fff5fffffffe) *)
+ := (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 "'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 "'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 "'0x1ffffffffffce'" (* 562949953421262 (0x1ffffffffffce) *)
:= (Const 562949953421262%Z).
Notation "'0x1ffffffffffce'" (* 562949953421262 (0x1ffffffffffce) *)
@@ -2610,6 +2673,10 @@ Notation "'0xfffffffffff45'" (* 4503599627370309 (0xfffffffffff45) *)
:= (Const 4503599627370309%Z).
Notation "'0xfffffffffff45'" (* 4503599627370309 (0xfffffffffff45) *)
:= (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~0~1~0~0~0~1~0~1).
+Notation "'0xfffffffffffc2'" (* 4503599627370434 (0xfffffffffffc2) *)
+ := (Const 4503599627370434%Z).
+Notation "'0xfffffffffffc2'" (* 4503599627370434 (0xfffffffffffc2) *)
+ := (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~0~0~0~1~0).
Notation "'0xfffffffffffda'" (* 4503599627370458 (0xfffffffffffda) *)
:= (Const 4503599627370458%Z).
Notation "'0xfffffffffffda'" (* 4503599627370458 (0xfffffffffffda) *)
@@ -2662,6 +2729,10 @@ Notation "'0x1ffffffffffff6'" (* 9007199254740982 (0x1ffffffffffff6) *)
:= (Const 9007199254740982%Z).
Notation "'0x1ffffffffffff6'" (* 9007199254740982 (0x1ffffffffffff6) *)
:= (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~1~1~0).
+Notation "'0x1ffffffffffffc'" (* 9007199254740988 (0x1ffffffffffffc) *)
+ := (Const 9007199254740988%Z).
+Notation "'0x1ffffffffffffc'" (* 9007199254740988 (0x1ffffffffffffc) *)
+ := (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~1~1~0~0).
Notation "'0x1ffffffffffffe'" (* 9007199254740990 (0x1ffffffffffffe) *)
:= (Const 9007199254740990%Z).
Notation "'0x1ffffffffffffe'" (* 9007199254740990 (0x1ffffffffffffe) *)
@@ -2826,6 +2897,10 @@ Notation "'0x1fffffffffffffb'" (* 144115188075855867 (0x1fffffffffffffb) *)
:= (Const 144115188075855867%Z).
Notation "'0x1fffffffffffffb'" (* 144115188075855867 (0x1fffffffffffffb) *)
:= (Const WO~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1).
+Notation "'0x1fffffffffffffc'" (* 144115188075855868 (0x1fffffffffffffc) *)
+ := (Const 144115188075855868%Z).
+Notation "'0x1fffffffffffffc'" (* 144115188075855868 (0x1fffffffffffffc) *)
+ := (Const WO~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0).
Notation "'0x1fffffffffffffd'" (* 144115188075855869 (0x1fffffffffffffd) *)
:= (Const 144115188075855869%Z).
Notation "'0x1fffffffffffffd'" (* 144115188075855869 (0x1fffffffffffffd) *)
@@ -2870,6 +2945,14 @@ Notation "'0x3fffffffffffff6'" (* 288230376151711734 (0x3fffffffffffff6) *)
:= (Const 288230376151711734%Z).
Notation "'0x3fffffffffffff6'" (* 288230376151711734 (0x3fffffffffffff6) *)
:= (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~1~0~1~1~0).
+Notation "'0x3fffffffffffffa'" (* 288230376151711738 (0x3fffffffffffffa) *)
+ := (Const 288230376151711738%Z).
+Notation "'0x3fffffffffffffa'" (* 288230376151711738 (0x3fffffffffffffa) *)
+ := (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~1~1~0~1~0).
+Notation "'0x3fffffffffffffc'" (* 288230376151711740 (0x3fffffffffffffc) *)
+ := (Const 288230376151711740%Z).
+Notation "'0x3fffffffffffffc'" (* 288230376151711740 (0x3fffffffffffffc) *)
+ := (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~1~1~1~0~0).
Notation "'0x3fffffffffffffd'" (* 288230376151711741 (0x3fffffffffffffd) *)
:= (Const 288230376151711741%Z).
Notation "'0x3fffffffffffffd'" (* 288230376151711741 (0x3fffffffffffffd) *)
@@ -2942,6 +3025,10 @@ Notation "'0xfffffffffffffda'" (* 1152921504606846938 (0xfffffffffffffda) *)
:= (Const 1152921504606846938%Z).
Notation "'0xfffffffffffffda'" (* 1152921504606846938 (0xfffffffffffffda) *)
:= (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
+Notation "'0xfffffffffffffde'" (* 1152921504606846942 (0xfffffffffffffde) *)
+ := (Const 1152921504606846942%Z).
+Notation "'0xfffffffffffffde'" (* 1152921504606846942 (0xfffffffffffffde) *)
+ := (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
Notation "'0xffffffffffffffe'" (* 1152921504606846974 (0xffffffffffffffe) *)
:= (Const 1152921504606846974%Z).
Notation "'0xffffffffffffffe'" (* 1152921504606846974 (0xffffffffffffffe) *)
@@ -2958,6 +3045,14 @@ Notation "'0x1000000000000001'" (* 1152921504606846977 (0x1000000000000001) *)
:= (Const 1152921504606846977%Z).
Notation "'0x1000000000000001'" (* 1152921504606846977 (0x1000000000000001) *)
:= (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~0~0~0~0~0~0~0~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 "'0x1ffffffffffffffc'" (* 2305843009213693948 (0x1ffffffffffffffc) *)
+ := (Const 2305843009213693948%Z).
+Notation "'0x1ffffffffffffffc'" (* 2305843009213693948 (0x1ffffffffffffffc) *)
+ := (Const WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0x1ffffffffffffffe'" (* 2305843009213693950 (0x1ffffffffffffffe) *)
+ := (Const 2305843009213693950%Z).
+Notation "'0x1ffffffffffffffe'" (* 2305843009213693950 (0x1ffffffffffffffe) *)
+ := (Const WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0x1fffffffffffffff'" (* 2305843009213693951 (0x1fffffffffffffff) *)
:= (Const 2305843009213693951%Z).
Notation "'0x1fffffffffffffff'" (* 2305843009213693951 (0x1fffffffffffffff) *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 13:01:55 +0000