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
Jonas Kastberg
iris
Commits
3b03bb6d
Commit
3b03bb6d
authored
Mar 04, 2018
by
Jacques-Henri Jourdan
Browse files
More Hint Modes.
parent
5392b62f
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/bi/derived_connectives.v
View file @
3b03bb6d
...
...
@@ -32,10 +32,12 @@ Arguments affine {_} _%I {_}.
Hint
Mode
Affine
+
!
:
typeclass_instances
.
Class
BiAffine
(
PROP
:
bi
)
:
=
absorbing_bi
(
Q
:
PROP
)
:
Affine
Q
.
Hint
Mode
BiAffine
!
:
typeclass_instances
.
Existing
Instance
absorbing_bi
|
0
.
Class
BiPositive
(
PROP
:
bi
)
:
=
bi_positive
(
P
Q
:
PROP
)
:
bi_affinely
(
P
∗
Q
)
⊢
bi_affinely
P
∗
Q
.
Hint
Mode
BiPositive
!
:
typeclass_instances
.
Definition
bi_absorbingly
{
PROP
:
bi
}
(
P
:
PROP
)
:
PROP
:
=
(
True
∗
P
)%
I
.
Arguments
bi_absorbingly
{
_
}
_
%
I
:
simpl
never
.
...
...
@@ -45,6 +47,7 @@ Typeclasses Opaque bi_absorbingly.
Class
Absorbing
{
PROP
:
bi
}
(
P
:
PROP
)
:
=
absorbing
:
bi_absorbingly
P
⊢
P
.
Arguments
Absorbing
{
_
}
_
%
I
:
simpl
never
.
Arguments
absorbing
{
_
}
_
%
I
.
Hint
Mode
Absorbing
+
!
:
typeclass_instances
.
Definition
bi_persistently_if
{
PROP
:
bi
}
(
p
:
bool
)
(
P
:
PROP
)
:
PROP
:
=
(
if
p
then
bi_persistently
P
else
P
)%
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