diff options
Diffstat (limited to 'src/Compilers/Z/HexNotationConstants.v')
| -rw-r--r-- | src/Compilers/Z/HexNotationConstants.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index 7c7554b39..3d952be63 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -111,6 +111,7 @@ nums = tuple(sorted(set(systematic_nums + [ 536870910, 678152731, 954437177, + 1054736383, 1065418751, 1073709055, 1073741821, @@ -1541,6 +1542,10 @@ Notation "'0x38e38e39'" (* 954437177 (0x38e38e39) *) := (Const 954437177%Z). Notation "'0x38e38e39'" (* 954437177 (0x38e38e39) *) := (Const WO~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~1). +Notation "'0x3eddffff'" (* 1054736383 (0x3eddffff) *) + := (Const 1054736383%Z). +Notation "'0x3eddffff'" (* 1054736383 (0x3eddffff) *) + := (Const WO~0~0~1~1~1~1~1~0~1~1~0~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0x3f80ffff'" (* 1065418751 (0x3f80ffff) *) := (Const 1065418751%Z). Notation "'0x3f80ffff'" (* 1065418751 (0x3f80ffff) *) |