Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Rice Wine
Iris
Commits
f31c5028
Commit
f31c5028
authored
May 31, 2018
by
Ralf Jung
Browse files
reserve embedding notation as well
parent
3d261c32
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/bi/notation.v
View file @
f31c5028
...
...
@@ -14,6 +14,8 @@ Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ
Reserved
Notation
"P ∗ Q"
(
at
level
80
,
right
associativity
).
Reserved
Notation
"P -∗ Q"
(
at
level
99
,
Q
at
level
200
,
right
associativity
).
Reserved
Notation
"⎡ P ⎤"
.
(** Modalities *)
Reserved
Notation
"'<pers>' P"
(
at
level
20
,
right
associativity
).
Reserved
Notation
"'<pers>?' p P"
(
at
level
20
,
p
at
level
9
,
P
at
level
20
,
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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