We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 6252fe1 commit d146ed7Copy full SHA for d146ed7
exercises/structured_conc.v
@@ -336,7 +336,7 @@ Context `{!heapGS Σ, !tokenG Σ}.
336
337
(**
338
It is actually quite straightforward to prove the [par] specification
339
- as most of the heavy lifting is done by [spawn_spec] and [par_spec].
+ as most of the heavy lifting is done by [spawn_spec] and [join_spec].
340
*)
341
Lemma par_spec (P1 P2 : iProp Σ) (e1 e2 : expr) (Q1 Q2 : val → iProp Σ) :
342
{{{ P1 }}} e1 {{{ v, RET v; Q1 v }}} -∗
0 commit comments