Commit b6192940 authored by Ralf Jung's avatar Ralf Jung

closed proofs: be more explicit about composed gFunctors

parent 3077c6c6
......@@ -57,10 +57,16 @@ Section client.
Qed.
End client.
Section ClosedProofs.
Definition Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
Lemma client_adequate σ : adequate client σ (λ _, True).
Proof.
apply (heap_adequacy #[ heapΣ ; barrierΣ ; spawnΣ ])=> ?.
apply (heap_adequacy Σ)=> ?.
apply (client_safe (nroot .@ "barrier")); auto with ndisj.
Qed.
Print Assumptions client_adequate.
End ClosedProofs.
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