From 17b5bd9afe6df83ca91e835b9b194e3da7c7865a Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 5 Dec 2017 10:49:27 +0100 Subject: [PATCH] Add notations for some of the new heap_lang binary operators. --- theories/heap_lang/notation.v | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v index 0ee932730..3751417fa 100644 --- a/theories/heap_lang/notation.v +++ b/theories/heap_lang/notation.v @@ -58,16 +58,21 @@ Notation "()" := LitUnit : val_scope. Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope. Notation "'ref' e" := (Alloc e%E) (at level 30, right associativity) : expr_scope. -Notation "- e" := (UnOp MinusUnOp e%E) - (at level 35, right associativity) : expr_scope. -Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E) - (at level 50, left associativity) : expr_scope. -Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E) - (at level 50, left associativity) : expr_scope. -Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E) (at level 70) : expr_scope. -Notation "e1 < e2" := (BinOp LtOp e1%E e2%E) (at level 70) : expr_scope. -Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) (at level 70) : expr_scope. -Notation "e1 ≠e2" := (UnOp NegOp (BinOp EqOp e1%E e2%E)) (at level 70) : expr_scope. +Notation "- e" := (UnOp MinusUnOp e%E) : expr_scope. + +Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E) : expr_scope. +Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E) : expr_scope. +Notation "e1 * e2" := (BinOp MultOp e1%E e2%E) : expr_scope. +Notation "e1 `quot` e2" := (BinOp QuotOp e1%E e2%E) : expr_scope. +Notation "e1 `rem` e2" := (BinOp RemOp e1%E e2%E) : expr_scope. +Notation "e1 ≪ e2" := (BinOp ShiftLOp e1%E e2%E) : expr_scope. +Notation "e1 ≫ e2" := (BinOp ShiftROp e1%E e2%E) : expr_scope. + +Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E) : expr_scope. +Notation "e1 < e2" := (BinOp LtOp e1%E e2%E) : expr_scope. +Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) : expr_scope. +Notation "e1 ≠e2" := (UnOp NegOp (BinOp EqOp e1%E e2%E)) : expr_scope. + Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope. (* The unicode ↠is already part of the notation "_ ↠_; _" for bind. *) Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope. -- GitLab