Skip to content

GitLab

Commit 8ebe1485 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add notation for pointer arithmetic to heap_lang.

parent 47f304f6
Pipeline #17347 passed with stage
in 13 minutes and 32 seconds
Hide whitespace changes
Inline Side-by-side
theories/heap_lang/notation.v
View file @ 8ebe1485
......@@ -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.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment