Commit a0bc4d00 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix.

parent 86f1cf3d
Pipeline #21267 passed with stage
in 5 minutes and 2 seconds
......@@ -171,7 +171,7 @@ Proof.
by iApply "HΦ".
Qed.
Lemma prog_fun_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
Lemma prog_loop_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
wp_apply (start_chan_proto_spec prot_loop); iIntros (c) "Hc".
......
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