aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Z/HexNotationConstants.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Compilers/Z/HexNotationConstants.v')
-rw-r--r--src/Compilers/Z/HexNotationConstants.v15
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) *)