list_reverse.8.9.ref 800 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12
1 subgoal
  
  Σ : gFunctors
  heapG0 : heapG Σ
  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
  --------------------------------------∗
13
  WP (rev hd) acc [{ v, Φ v }]
14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
  
1 subgoal
  
  Σ : gFunctors
  heapG0 : heapG Σ
  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
31
       "l" <- ("tmp1", acc);; (rev "tmp2") (InjLV #())
32 33
     end [{ v, Φ v }]