heap_lang2.ref 315 Bytes
Newer Older
1 2 3
1 subgoal
  
  Σ : gFunctors
4
  heapG0 : heapG Σ
5 6 7 8 9 10 11 12
  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 }}