diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-14 22:27:34 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-14 22:27:34 -0400 |
| commit | f367c9ee36881feb001a411a2628482a44dec6fa (patch) | |
| tree | 9fa5e90b99f6ef552486a24ada1fdb15d6d7c442 /src/Compilers | |
| parent | 72a84fc5e7e7835608ad722c6c1a79e7067cc4a9 (diff) | |
Add reserved java notation
Diffstat (limited to 'src/Compilers')
| -rw-r--r-- | src/Compilers/Z/JavaNotations.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Compilers/Z/JavaNotations.v b/src/Compilers/Z/JavaNotations.v index 5d5964a82..99fa298e8 100644 --- a/src/Compilers/Z/JavaNotations.v +++ b/src/Compilers/Z/JavaNotations.v @@ -5,6 +5,7 @@ Require Export Crypto.Util.Notations. Reserved Notation "T x = A ; b" (at level 200, b at level 200, format "T x = A ; '//' b"). Reserved Notation "T0 x , T1 y = A ; b" (at level 200, b at level 200, format "T0 x , T1 y = A ; '//' b"). +Reserved Notation "v == 0 ? a : b" (at level 40, a at level 10, b at level 10). Reserved Notation "x & y" (at level 40). (* N.B. M32 is 0xFFFFFFFFL, and is how to cast a 64-bit thing to a 32-bit thing in Java *) Reserved Notation "'M32' & x" (at level 200, x at level 9). |