From 8ebe1485d2e6c90d90ffd61bfc0da71da1fba4ef Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 11 Jun 2019 08:48:35 +0200 Subject: [PATCH] Add notation for pointer arithmetic to heap_lang. --- theories/heap_lang/notation.v | 1 + 1 file changed, 1 insertion(+) diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v index 891059eba..420fb7154 100644 --- a/theories/heap_lang/notation.v +++ b/theories/heap_lang/notation.v @@ -60,6 +60,7 @@ Notation "'ref' e" := (Alloc e%E) (at level 10) : 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 OffsetOp 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. -- GitLab