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
bf9fd4f5
Commit
bf9fd4f5
authored
Jun 14, 2018
by
Ralf Jung
Browse files
allow FrameMonPredAt to infer the index
parent
8d3d9514
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/proofmode/monpred.v
View file @
bf9fd4f5
...
...
@@ -21,7 +21,7 @@ Class FrameMonPredAt {I : biIndex} {PROP : bi} (p : bool) (i : I)
(
𝓡
:
PROP
)
(
P
:
monPred
I
PROP
)
(
𝓠
:
PROP
)
:
=
frame_monPred_at
:
□
?p
𝓡
∗
𝓠
-
∗
P
i
.
Arguments
FrameMonPredAt
{
_
_
}
_
_
_
%
I
_
%
I
_
%
I
.
Hint
Mode
FrameMonPredAt
+
+
+
+
!
!
-
:
typeclass_instances
.
Hint
Mode
FrameMonPredAt
+
+
+
-
!
!
-
:
typeclass_instances
.
Section
modalities
.
Context
{
I
:
biIndex
}
{
PROP
:
bi
}.
...
...
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