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
30
31
32
|
1 goal
Σ : gFunctors
heapGS0 : heapGS Σ
hd, acc : val
xs, ys : list val
Φ : val → iPropI Σ
============================
"Hxs" : is_list hd xs
"Hys" : is_list acc ys
"HΦ" : ∀ w : val, is_list w (reverse xs ++ ys) -∗ Φ w
--------------------------------------∗
WP rev hd acc [{ v, Φ v }]
1 goal
Σ : gFunctors
heapGS0 : heapGS Σ
acc : val
ys : list val
Φ : val → iPropI Σ
============================
"Hys" : is_list acc ys
"HΦ" : ∀ w : val, is_list w ys -∗ Φ w
--------------------------------------∗
WP match: InjLV #() with
InjL <> => acc
| InjR "l" =>
let: "tmp1" := Fst ! "l" in
let: "tmp2" := Snd ! "l" in
"l" <- ("tmp1", acc);; rev "tmp2" (InjLV #())
end
[{ v, Φ v }]
|
