1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
1 goal
Σ : gFunctors
heapGS0 : heapGS Σ
P, Q : iProp Σ
============================
P ={⊤}=∗ Q
1 goal
Σ : gFunctors
heapGS0 : heapGS Σ
fun1, fun2, fun3 : expr
============================
--------------------------------------∗
WP let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
{{ _, True }}
1 goal
Σ : gFunctors
heapGS0 : heapGS Σ
fun1, fun2, fun3 : expr
============================
{{{ True }}}
let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
{{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
|
