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
Jonas Kastberg
iris
Commits
436f4abe
Commit
436f4abe
authored
Feb 06, 2020
by
Ralf Jung
Browse files
cancellable -> cancelable
parent
b8d083f2
Changes
1
Show whitespace changes
Inline
Side-by-side
theories/bi/lib/counterexamples.v
View file @
436f4abe
...
@@ -234,7 +234,7 @@ Module linear1. Section linear1.
...
@@ -234,7 +234,7 @@ Module linear1. Section linear1.
Hypothesis
fupd_fupd
:
∀
E1
E2
E3
P
,
fupd
E1
E2
(
fupd
E2
E3
P
)
⊢
fupd
E1
E3
P
.
Hypothesis
fupd_fupd
:
∀
E1
E2
E3
P
,
fupd
E1
E2
(
fupd
E2
E3
P
)
⊢
fupd
E1
E3
P
.
Hypothesis
fupd_frame_l
:
∀
E1
E2
P
Q
,
P
∗
fupd
E1
E2
Q
⊢
fupd
E1
E2
(
P
∗
Q
).
Hypothesis
fupd_frame_l
:
∀
E1
E2
P
Q
,
P
∗
fupd
E1
E2
Q
⊢
fupd
E1
E2
(
P
∗
Q
).
(** We have cancel
l
able invariants. (Really they would have fractions at
(** We have cancelable invariants. (Really they would have fractions at
[cinv_own] but we do not need that. They would also have a name matching
[cinv_own] but we do not need that. They would also have a name matching
the [mask] type, but we do not need that either.) *)
the [mask] type, but we do not need that either.) *)
Context
(
gname
:
Type
)
(
cinv
:
gname
→
PROP
→
PROP
)
(
cinv_own
:
gname
→
PROP
).
Context
(
gname
:
Type
)
(
cinv
:
gname
→
PROP
→
PROP
)
(
cinv_own
:
gname
→
PROP
).
...
@@ -288,7 +288,7 @@ Module linear2. Section linear2.
...
@@ -288,7 +288,7 @@ Module linear2. Section linear2.
Hypothesis
fupd_fupd
:
∀
E1
E2
E3
P
,
fupd
E1
E2
(
fupd
E2
E3
P
)
⊢
fupd
E1
E3
P
.
Hypothesis
fupd_fupd
:
∀
E1
E2
E3
P
,
fupd
E1
E2
(
fupd
E2
E3
P
)
⊢
fupd
E1
E3
P
.
Hypothesis
fupd_frame_l
:
∀
E1
E2
P
Q
,
P
∗
fupd
E1
E2
Q
⊢
fupd
E1
E2
(
P
∗
Q
).
Hypothesis
fupd_frame_l
:
∀
E1
E2
P
Q
,
P
∗
fupd
E1
E2
Q
⊢
fupd
E1
E2
(
P
∗
Q
).
(** We have cancel
l
able invariants. (Really they would have fractions at
(** We have cancelable invariants. (Really they would have fractions at
[cinv_own] but we do not need that. They would also have a name matching
[cinv_own] but we do not need that. They would also have a name matching
the [mask] type, but we do not need that either.) *)
the [mask] type, but we do not need that either.) *)
Context
(
gname
:
Type
)
(
cinv
:
gname
→
PROP
→
PROP
)
(
cinv_own
:
gname
→
PROP
).
Context
(
gname
:
Type
)
(
cinv
:
gname
→
PROP
→
PROP
)
(
cinv_own
:
gname
→
PROP
).
...
...
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