diff options
Diffstat (limited to 'src/Compilers/Z/BinaryNotationConstants.v')
| -rw-r--r-- | src/Compilers/Z/BinaryNotationConstants.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v index eb05ffaba..0f918aca4 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -72,6 +72,8 @@ nums = tuple(sorted(set(systematic_nums + [ 2097135, 2097143, 2097150, + 4120062, + 4162878, 4188670, 4192254, 4193327, @@ -991,6 +993,10 @@ Notation "'0b1000000000000000000000'" (* 2097152 (0x200000) *) := (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). Notation "'0b1000000000000000000001'" (* 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 "'0b1111101101110111111110'" (* 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 "'0b1111111000010100111110'" (* 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 "'0b1111111110100111111110'" (* 4188670 (0x3fe9fe) *) := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~0~1~0~0~1~1~1~1~1~1~1~1~0). Notation "'0b1111111111011111111110'" (* 4192254 (0x3ff7fe) *) |