diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-02 01:22:13 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-02 01:22:13 -0400 |
| commit | 7a5265682957414a49e3e650c5c56bf5482f2fd0 (patch) | |
| tree | 78aa5332ba97a62fbe954a9a565b5fd4cab1a755 /src/Compilers/Z/BinaryNotationConstants.v | |
| parent | 743f894f247b56f39e16324f480d6307b3db3842 (diff) | |
Add more constant notations
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 cf188caaf..739c17146 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -131,6 +131,8 @@ nums = tuple(sorted(set(systematic_nums + [ 4294963199, 4294966319, 4294966531, + 4294966727, + 4294966815, 4294966875, 4294966979, 4294967107, @@ -1001,6 +1003,10 @@ Notation "'0b11111111111111111111110000101111'" (* 4294966319 (0xfffffc2f) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1). Notation "'0b11111111111111111111110100000011'" (* 4294966531 (0xfffffd03) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~0~0~1~1). +Notation "'0b11111111111111111111110111000111'" (* 4294966727 (0xfffffdc7) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1). +Notation "'0b11111111111111111111111000011111'" (* 4294966815 (0xfffffe1f) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1). Notation "'0b11111111111111111111111001011011'" (* 4294966875 (0xfffffe5b) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~0~1~1). Notation "'0b11111111111111111111111011000011'" (* 4294966979 (0xfffffec3) *) |