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
Janno
iris-coq
Commits
3d261c32
Commit
3d261c32
authored
May 31, 2018
by
Ralf Jung
Browse files
also reserve monPred modalities
parent
75236abc
Changes
2
Hide whitespace changes
Inline
Side-by-side
theories/bi/monpred.v
View file @
3d261c32
...
...
@@ -214,8 +214,8 @@ End Bi.
Arguments
monPred_objectively
{
_
_
}
_
%
I
.
Arguments
monPred_subjectively
{
_
_
}
_
%
I
.
Notation
"'<obj>' P"
:
=
(
monPred_objectively
P
)
(
at
level
20
,
right
associativity
)
:
bi_scope
.
Notation
"'<subj>' P"
:
=
(
monPred_subjectively
P
)
(
at
level
20
,
right
associativity
)
:
bi_scope
.
Notation
"'<obj>' P"
:
=
(
monPred_objectively
P
)
:
bi_scope
.
Notation
"'<subj>' P"
:
=
(
monPred_subjectively
P
)
:
bi_scope
.
Section
Sbi
.
Context
{
I
:
biIndex
}
{
PROP
:
sbi
}.
...
...
theories/bi/notation.v
View file @
3d261c32
...
...
@@ -43,6 +43,9 @@ Reserved Notation "■ P" (at level 20, right associativity).
Reserved
Notation
"■? p P"
(
at
level
20
,
p
at
level
9
,
P
at
level
20
,
right
associativity
,
format
"■? p P"
).
Reserved
Notation
"'<obj>' P"
(
at
level
20
,
right
associativity
).
Reserved
Notation
"'<subj>' P"
(
at
level
20
,
right
associativity
).
(** Update modalities *)
Reserved
Notation
"|==> Q"
(
at
level
99
,
Q
at
level
200
,
format
"|==> Q"
).
Reserved
Notation
"P ==∗ Q"
(
at
level
99
,
Q
at
level
200
,
format
"P ==∗ Q"
).
...
...
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