diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-14 17:15:27 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-14 17:15:27 -0400 |
| commit | 56a316ad7340ce6914c14e204918308463826b61 (patch) | |
| tree | 3113de60206e43cb71b3c0f4b42de9aebca5406b /src/Compilers/Z/JavaNotations.v | |
| parent | 7af112e5c46bc915b3209d28184ef2f90bf37aef (diff) | |
Add constant, support pair-returning assignment
Diffstat (limited to 'src/Compilers/Z/JavaNotations.v')
| -rw-r--r-- | src/Compilers/Z/JavaNotations.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Compilers/Z/JavaNotations.v b/src/Compilers/Z/JavaNotations.v index c14787e02..5d5964a82 100644 --- a/src/Compilers/Z/JavaNotations.v +++ b/src/Compilers/Z/JavaNotations.v @@ -4,6 +4,7 @@ Require Export Crypto.Compilers.Z.HexNotationConstants. 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 "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). @@ -11,6 +12,7 @@ Reserved Notation "'M32' & x" (at level 200, x at level 9). Global Open Scope expr_scope. Notation "T x = A ; b" := (LetIn (tx:=T) A (fun x => b)) : expr_scope. +Notation "T0 x , T1 y = A ; b" := (LetIn (tx:=Prod T0 T1) A (fun '((x, y)%core) => b)) : expr_scope. (* ??? Did I get M32 wrong? *) (*Notation "'(int)' x" := (Op (Cast _ (TWord 0)) x). Notation "'(int)' x" := (Op (Cast _ (TWord 1)) x). |