diff options
Diffstat (limited to 'src/Compilers/Z/HexNotationConstants.v')
-rw-r--r-- | src/Compilers/Z/HexNotationConstants.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index 9d6abe422..b818b97d7 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -60,6 +60,9 @@ WO~0~0~0~1~1~0~1~1 WO~0~0~0~1~1~1~0~0 WO~0~0~1~1~0~0~1~1 WO~0~1~0~1~0~1~0~1 +WO~1~0~0~0~0~0~0~0 +WO~1~0~0~0~0~0~0 +WO~1~0~0~0~0~0 WO~1~1~1~0~0~0 WO~0~1~0~1 WO~1~0~0~1 @@ -122,6 +125,10 @@ Notation "'0x1c'" (* 28 (0x1c) *) := (Const 28%Z). Notation "'0x1c'" (* 28 (0x1c) *) := (Const WO~0~0~0~1~1~1~0~0). +Notation "'0x20'" (* 32 (0x20) *) + := (Const 32%Z). +Notation "'0x20'" (* 32 (0x20) *) + := (Const WO~1~0~0~0~0~0). Notation "'0x33'" (* 51 (0x33) *) := (Const 51%Z). Notation "'0x33'" (* 51 (0x33) *) @@ -130,10 +137,18 @@ Notation "'0x38'" (* 56 (0x38) *) := (Const 56%Z). Notation "'0x38'" (* 56 (0x38) *) := (Const WO~1~1~1~0~0~0). +Notation "'0x40'" (* 64 (0x40) *) + := (Const 64%Z). +Notation "'0x40'" (* 64 (0x40) *) + := (Const WO~1~0~0~0~0~0~0). Notation "'0x55'" (* 85 (0x55) *) := (Const 85%Z). Notation "'0x55'" (* 85 (0x55) *) := (Const WO~0~1~0~1~0~1~0~1). +Notation "'0x80'" (* 128 (0x80) *) + := (Const 128%Z). +Notation "'0x80'" (* 128 (0x80) *) + := (Const WO~1~0~0~0~0~0~0~0). Notation "'0x1db41'" (* 121665 (0x1db41) *) := (Const 121665%Z). Notation "'0x1db41'" (* 121665 (0x1db41) *) |