Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Iris
Commits
17b5bd9a
Commit
17b5bd9a
authored
Dec 05, 2017
by
Robbert Krebbers
Browse files
Add notations for some of the new heap_lang binary operators.
parent
4782352f
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/heap_lang/notation.v
View file @
17b5bd9a
...
...
@@ -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
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment