Skip to content
Snippets Groups Projects
Commit 7fef7ccb authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make better use of `wp_smart_apply`.

parent b62c61b1
No related branches found
No related tags found
No related merge requests found
Pipeline #42011 passed
Hide whitespace changes
Inline Side-by-side
theories/examples/basics.v
+ 3
− 3
View file @ 7fef7ccb
...@@ -284,7 +284,7 @@ Proof. ...@@ -284,7 +284,7 @@ Proof.
wp_smart_apply (start_chan_spec prot_loop); iIntros (c) "Hc". wp_smart_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
- iLöb as "IH". - iLöb as "IH".
wp_recv (x) as "_". wp_send with "[//]". wp_recv (x) as "_". wp_send with "[//]".
do 2 wp_pure _. by iApply "IH". by wp_smart_apply "IH".
- wp_send with "[//]". wp_recv as "_". wp_send with "[//]". wp_recv as "_". - wp_send with "[//]". wp_recv as "_". wp_send with "[//]". wp_recv as "_".
wp_pures. by iApply "HΦ". wp_pures. by iApply "HΦ".
Qed. Qed.
...@@ -355,7 +355,7 @@ Proof. ...@@ -355,7 +355,7 @@ Proof.
wp_smart_apply (start_chan_spec prot_loop); iIntros (c) "Hc". wp_smart_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
- iLöb as "IH". - iLöb as "IH".
wp_recv (x) as "_". wp_send with "[//]". wp_recv (x) as "_". wp_send with "[//]".
do 2 wp_pure _. by iApply "IH". by wp_smart_apply "IH".
- wp_send with "[//]". wp_send with "[//]". wp_recv as "_". wp_recv as "_". - wp_send with "[//]". wp_send with "[//]". wp_recv as "_". wp_recv as "_".
wp_pures. by iApply "HΦ". wp_pures. by iApply "HΦ".
Qed. Qed.
...@@ -369,7 +369,7 @@ Proof. ...@@ -369,7 +369,7 @@ Proof.
wp_smart_apply (start_chan_spec prot_ref_loop); iIntros (c) "Hc". wp_smart_apply (start_chan_spec prot_ref_loop); iIntros (c) "Hc".
- iLöb as "IH". wp_lam. - iLöb as "IH". wp_lam.
wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[$Hl]". wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[$Hl]".
do 2 wp_pure _. by iApply "IH". by wp_smart_apply "IH".
- wp_alloc l1 as "Hl1". wp_alloc l2 as "Hl2". - wp_alloc l1 as "Hl1". wp_alloc l2 as "Hl2".
wp_send with "[$Hl1]". wp_send with "[$Hl2]". wp_send with "[$Hl1]". wp_send with "[$Hl2]".
wp_recv as "Hl1". wp_recv as "Hl2". wp_recv as "Hl1". wp_recv as "Hl2".
......
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