diff options
Diffstat (limited to 'src/Compilers/Z/HexNotationConstants.v')
| -rw-r--r-- | src/Compilers/Z/HexNotationConstants.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index 4958fe902..3a76165f5 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -72,6 +72,8 @@ nums = tuple(sorted(set(systematic_nums + [ 2097135, 2097143, 2097150, + 4120062, + 4162878, 4188670, 4192254, 4193327, @@ -1449,6 +1451,14 @@ Notation "'0x200001'" (* 2097153 (0x200001) *) := (Const 2097153%Z). Notation "'0x200001'" (* 2097153 (0x200001) *) := (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~1). +Notation "'0x3eddfe'" (* 4120062 (0x3eddfe) *) + := (Const 4120062%Z). +Notation "'0x3eddfe'" (* 4120062 (0x3eddfe) *) + := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~0~1~1~0~1~1~1~0~1~1~1~1~1~1~1~1~0). +Notation "'0x3f853e'" (* 4162878 (0x3f853e) *) + := (Const 4162878%Z). +Notation "'0x3f853e'" (* 4162878 (0x3f853e) *) + := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~0~0~0~1~0~1~0~0~1~1~1~1~1~0). Notation "'0x3fe9fe'" (* 4188670 (0x3fe9fe) *) := (Const 4188670%Z). Notation "'0x3fe9fe'" (* 4188670 (0x3fe9fe) *) |