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
Pierre-Marie Pédrot
Iris
Commits
c9ae33d4
Commit
c9ae33d4
authored
Jan 18, 2016
by
Robbert Krebbers
Browse files
Fix typo in scopes for notations of triples.
parent
254989a5
Changes
1
Show whitespace changes
Inline
Side-by-side
iris/hoare.v
View file @
c9ae33d4
...
@@ -6,9 +6,9 @@ Definition ht {Σ} (E : coPset) (P : iProp Σ)
...
@@ -6,9 +6,9 @@ Definition ht {Σ} (E : coPset) (P : iProp Σ)
Instance
:
Params
(@
ht
)
2
.
Instance
:
Params
(@
ht
)
2
.
Notation
"{{ P } } e @ E {{ Q } }"
:
=
(
ht
E
P
e
Q
)
Notation
"{{ P } } e @ E {{ Q } }"
:
=
(
ht
E
P
e
Q
)
(
at
level
74
,
format
"{{ P } } e @ E {{ Q } }"
)
:
C
_scope
.
(
at
level
74
,
format
"{{ P } } e @ E {{ Q } }"
)
:
uPred
_scope
.
Notation
"{{ P } } e @ E {{ Q } }"
:
=
(
True
⊑
ht
E
P
e
Q
)
Notation
"{{ P } } e @ E {{ Q } }"
:
=
(
True
⊑
ht
E
P
e
Q
)
(
at
level
74
,
format
"{{ P } } e @ E {{ Q } }"
)
:
type
_scope
.
(
at
level
74
,
format
"{{ P } } e @ E {{ Q } }"
)
:
C
_scope
.
Section
hoare
.
Section
hoare
.
Context
{
Σ
:
iParam
}.
Context
{
Σ
:
iParam
}.
...
...
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