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
c984a2bc
Commit
c984a2bc
authored
Nov 21, 2017
by
Ralf Jung
Browse files
use a more descriptive tactic
parent
a51a6e3e
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/heap_lang/lib/spin_lock.v
View file @
c984a2bc
...
...
@@ -49,7 +49,7 @@ Section proof.
{{{
R
}}}
newlock
#()
{{{
lk
γ
,
RET
lk
;
is_lock
γ
lk
R
}}}.
Proof
.
iIntros
(
Φ
)
"HR HΦ"
.
rewrite
-
wp_fupd
/
newlock
/=.
wp_
seq
.
wp_alloc
l
as
"Hl"
.
wp_
lam
.
wp_alloc
l
as
"Hl"
.
iMod
(
own_alloc
(
Excl
()))
as
(
γ
)
"Hγ"
;
first
done
.
iMod
(
inv_alloc
N
_
(
lock_inv
γ
l
R
)
with
"[-HΦ]"
)
as
"#?"
.
{
iIntros
"!>"
.
iExists
false
.
by
iFrame
.
}
...
...
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