Skip to content
Snippets Groups Projects
Commit 20aef084 authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Removed redundant unit in example

parent e1e9c9d9
No related branches found
No related tags found
No related merge requests found
Pipeline #39419 passed
Hide whitespace changes
Inline Side-by-side
theories/logrel/examples/compute_client_list.v
+ 2
− 2
View file @ 20aef084
...@@ -25,7 +25,7 @@ From actris.logrel.examples Require Import compute_service. ...@@ -25,7 +25,7 @@ From actris.logrel.examples Require Import compute_service.
Definition send_all_par : val := Definition send_all_par : val :=
rec: "go" "c" "xs" "lk" "counter" := rec: "go" "c" "xs" "lk" "counter" :=
if: lisnil "xs" then if: lisnil "xs" then
acquire "lk";; select "c" #stop;; release "lk";; #() acquire "lk";; select "c" #stop;; release "lk"
else else
acquire "lk";; acquire "lk";;
select "c" #cont;; send "c" (lpop "xs");; select "c" #cont;; send "c" (lpop "xs");;
...@@ -187,7 +187,7 @@ Section compute_example. ...@@ -187,7 +187,7 @@ Section compute_example.
iExists n, false. iExists n, false.
rewrite lookup_total_insert -lsty_car_app lty_app_end_l lty_app_end_r. rewrite lookup_total_insert -lsty_car_app lty_app_end_l lty_app_end_r.
iFrame "Hf Hcounter Hc". } iFrame "Hf Hcounter Hc". }
iIntros "_". wp_pures. iApply "HΦ". by iFrame "Hl Hlk". } iIntros "_". iApply "HΦ". by iFrame "Hl Hlk". }
wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl". wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
wp_apply (acquire_spec with "Hlk"). wp_apply (acquire_spec with "Hlk").
iIntros "[Hlocked HI]". iIntros "[Hlocked HI]".
......
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