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
Adam
Iris
Commits
ecd4e746
Commit
ecd4e746
authored
Feb 19, 2021
by
Jan-Oliver Kaiser
Browse files
Enable `Typeclasses Strict Resolution` for dervied_connectives.v
parent
5bb93f57
Changes
1
Hide whitespace changes
Inline
Side-by-side
iris/bi/derived_connectives.v
View file @
ecd4e746
...
...
@@ -13,6 +13,8 @@ Global Arguments bi_wand_iff {_} _%I _%I : simpl never.
Global
Instance
:
Params
(@
bi_wand_iff
)
1
:
=
{}.
Infix
"∗-∗"
:
=
bi_wand_iff
:
bi_scope
.
#[
local
]
Set
Typeclasses
Strict
Resolution
.
Class
Persistent
{
PROP
:
bi
}
(
P
:
PROP
)
:
=
persistent
:
P
⊢
<
pers
>
P
.
Global
Arguments
Persistent
{
_
}
_
%
I
:
simpl
never
.
Global
Arguments
persistent
{
_
}
_
%
I
{
_
}.
...
...
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