Commit ea355392 authored by Ralf Jung's avatar Ralf Jung

forgot to update reference output

parent 51afb8bd
......@@ -30,6 +30,33 @@
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
{{ _, True }}
1 subgoal
Σ : gFunctors
H : heapG Σ
fun1, fun2, fun3 : expr
Φ : language.val heap_lang → iProp Σ
============================
--------------------------------------∗
WP let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
{{ v, Φ v }}
1 subgoal
Σ : gFunctors
H : heapG Σ
fun1, fun2, fun3 : expr
Φ : language.val heap_lang → iProp Σ
E : coPset
============================
--------------------------------------∗
WP let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
@ E {{ v, Φ v }}
1 subgoal
Σ : gFunctors
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment