Forked from
Iris / Iris
1422 commits behind the upstream repository.
heap_lang_printing2.ref 744 B
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 }}}