From 8fd656355fddcc017af3064db74b1ecf3eabdf2c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 12 Nov 2017 22:17:37 -0500 Subject: Add more constant notations --- src/Compilers/Z/BinaryNotationConstants.v | 138 ++++++++++++++++++ src/Compilers/Z/HexNotationConstants.v | 230 ++++++++++++++++++++++++++++++ 2 files changed, 368 insertions(+) (limited to 'src') 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) *) -- cgit v1.2.3