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
Rodolphe Lepigre
Iris
Commits
11e0f153
Commit
11e0f153
authored
Nov 29, 2017
by
Robbert Krebbers
Browse files
Add a test-case.
parent
7453ecb0
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/tests/heap_lang.v
View file @
11e0f153
...
...
@@ -10,6 +10,16 @@ Section LiftingTests.
Implicit
Types
P
Q
:
iProp
Σ
.
Implicit
Types
Φ
:
val
→
iProp
Σ
.
Definition
simpl_test
:
⌜
(
10
=
4
+
6
)%
nat
⌝
-
∗
WP
let
:
"x"
:
=
ref
#
1
in
"x"
<-
!
"x"
;;
!
"x"
{{
v
,
⌜
v
=
#
1
⌝
}}.
Proof
.
iIntros
"?"
.
wp_alloc
l
.
repeat
(
wp_pure
_
)
||
wp_load
||
wp_store
.
match
goal
with
|
|-
context
[
(
10
=
4
+
6
)%
nat
]
=>
done
end
.
Qed
.
Definition
heap_e
:
expr
:
=
let
:
"x"
:
=
ref
#
1
in
"x"
<-
!
"x"
+
#
1
;;
!
"x"
.
...
...
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