Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Jonas Kastberg
iris
Commits
75e30fd5
Commit
75e30fd5
authored
Apr 05, 2018
by
Ralf Jung
Browse files
fix notation conflict
parent
b3af10b3
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/bi/interface.v
View file @
75e30fd5
...
...
@@ -3,8 +3,10 @@ Set Primitive Projections.
Reserved
Notation
"P ⊢ Q"
(
at
level
99
,
Q
at
level
200
,
right
associativity
).
Reserved
Notation
"P '⊢@{' PROP } Q"
(
at
level
99
,
Q
at
level
200
,
right
associativity
).
Reserved
Notation
"('⊢@{' PROP } )"
(
at
level
99
).
Reserved
Notation
"P ⊣⊢ Q"
(
at
level
95
,
no
associativity
).
Reserved
Notation
"P '⊣⊢@{' PROP } Q"
(
at
level
95
,
no
associativity
).
Reserved
Notation
"('⊣⊢@{' PROP } )"
(
at
level
95
).
Reserved
Notation
"'emp'"
.
Reserved
Notation
"'⌜' φ '⌝'"
(
at
level
1
,
φ
at
level
200
,
format
"⌜ φ ⌝"
).
Reserved
Notation
"P ∗ Q"
(
at
level
80
,
right
associativity
).
...
...
@@ -270,12 +272,12 @@ Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
Notation
"P ⊢ Q"
:
=
(
bi_entails
P
%
I
Q
%
I
)
:
stdpp_scope
.
Notation
"P ⊢@{ PROP } Q"
:
=
(
bi_entails
(
PROP
:
=
PROP
)
P
%
I
Q
%
I
)
(
only
parsing
)
:
stdpp_scope
.
Notation
"(⊢)"
:
=
bi_entails
(
only
parsing
)
:
stdpp_scope
.
Notation
"(⊢@{ PROP })"
:
=
(
bi_entails
(
PROP
:
=
PROP
))
(
only
parsing
)
:
stdpp_scope
.
Notation
"(⊢@{ PROP }
)"
:
=
(
bi_entails
(
PROP
:
=
PROP
))
(
only
parsing
)
:
stdpp_scope
.
Notation
"P ⊣⊢ Q"
:
=
(
equiv
(
A
:
=
bi_car
_
)
P
%
I
Q
%
I
)
:
stdpp_scope
.
Notation
"P ⊣⊢@{ PROP } Q"
:
=
(
equiv
(
A
:
=
bi_car
PROP
)
P
%
I
Q
%
I
)
(
only
parsing
)
:
stdpp_scope
.
Notation
"(⊣⊢)"
:
=
(
equiv
(
A
:
=
bi_car
_
))
(
only
parsing
)
:
stdpp_scope
.
Notation
"(⊣⊢@{ PROP })"
:
=
(
equiv
(
A
:
=
bi_car
PROP
))
(
only
parsing
)
:
stdpp_scope
.
Notation
"(⊣⊢@{ PROP }
)"
:
=
(
equiv
(
A
:
=
bi_car
PROP
))
(
only
parsing
)
:
stdpp_scope
.
Notation
"P -∗ Q"
:
=
(
P
⊢
Q
)
:
stdpp_scope
.
...
...
Write
Preview
Supports
Markdown
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