Commit 37145a3b by Ralf Jung

### fix lecture_notes

parent c75b4277
Pipeline #14818 passed with stage
in 11 minutes and 56 seconds
 ... @@ -140,7 +140,7 @@ Section proof. ... @@ -140,7 +140,7 @@ Section proof. called wp_par. The two arguments are the conclusions of the two called wp_par. The two arguments are the conclusions of the two parallel threads. Here they are simply True, as in the paper proof when parallel threads. Here they are simply True, as in the paper proof when we used the ht-par rule. *) we used the ht-par rule. *) iApply (wp_par (λ _ , ⌜True⌝)%I (λ _ , ⌜True⌝)%I). wp_apply (wp_par (λ _ , ⌜True⌝)%I (λ _ , ⌜True⌝)%I). (* We now have three subgoals. The first two are proofs that each thread (* We now have three subgoals. The first two are proofs that each thread does the correct thing, and the final goal is to show that the combined does the correct thing, and the final goal is to show that the combined conclusion of the two threads implies the desired conclusion. This last conclusion of the two threads implies the desired conclusion. This last ... ...
 ... @@ -280,7 +280,7 @@ Section example_1. ... @@ -280,7 +280,7 @@ Section example_1. wp_let. wp_let. wp_bind (_ ||| _)%E. wp_bind (_ ||| _)%E. let tac := iApply ("HIncr" with "[\$HInc]"); iNext; by iIntros (?) "_" in let tac := iApply ("HIncr" with "[\$HInc]"); iNext; by iIntros (?) "_" in iApply (wp_par (λ _, True%I) (λ _, True%I)); [tac | tac | ]. wp_apply (wp_par (λ _, True%I) (λ _, True%I)); [tac | tac | ]. { iIntros (v1 v2) "_ !>". { iIntros (v1 v2) "_ !>". wp_seq. wp_seq. wp_apply (read_spec _ _ _ True%I (λ _, True%I)); auto. wp_apply (read_spec _ _ _ True%I (λ _, True%I)); auto. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!