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
Iris
Iris
Commits
82b8ee7d
Commit
82b8ee7d
authored
Apr 07, 2022
by
Robbert Krebbers
Browse files
Comments.
parent
8845003c
Pipeline
#64443
passed with stage
in 7 minutes and 39 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
iris/base_logic/upred.v
View file @
82b8ee7d
...
...
@@ -435,6 +435,8 @@ Implicit Types A : Type.
Local
Arguments
uPred_holds
{
_
}
!
_
_
_
/.
Local
Hint
Immediate
uPred_in_entails
:
core
.
(** The notations below are implicitly local due to the section, so we do not
mind the overlap with the general BI notations. *)
Notation
"P ⊢ Q"
:
=
(@
uPred_entails
M
P
%
I
Q
%
I
)
:
stdpp_scope
.
Notation
"(⊢)"
:
=
(@
uPred_entails
M
)
(
only
parsing
)
:
stdpp_scope
.
Notation
"P ⊣⊢ Q"
:
=
(@
uPred_equiv
M
P
%
I
Q
%
I
)
:
stdpp_scope
.
...
...
iris/si_logic/siprop.v
View file @
82b8ee7d
...
...
@@ -128,6 +128,8 @@ Ltac unseal := rewrite !unseal_eqs /=.
Section
primitive
.
Local
Arguments
siProp_holds
!
_
_
/.
(** The notations below are implicitly local due to the section, so we do not
mind the overlap with the general BI notations. *)
Notation
"P ⊢ Q"
:
=
(
siProp_entails
P
Q
).
Notation
"'True'"
:
=
(
siProp_pure
True
)
:
bi_scope
.
Notation
"'False'"
:
=
(
siProp_pure
False
)
:
bi_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