Skip to content

GitLab

Commit 3477ed59 authored by Ralf Jung's avatar Ralf Jung
Browse files

re-add a TODO that has not been solved

parent 6f23f44e
Show whitespace changes
Inline Side-by-side
barrier/barrier.v
View file @ 3477ed59
...@@ -180,7 +180,9 @@ Section proof. ...@@ -180,7 +180,9 @@ Section proof.
(∃ γ, barrier_ctx γ l P ★ sts_ownS γ low_states {[ Send ]})%I. (∃ γ, barrier_ctx γ l P ★ sts_ownS γ low_states {[ Send ]})%I.
Global Instance send_ne n l : Proper (dist n ==> dist n) (send l). Global Instance send_ne n l : Proper (dist n ==> dist n) (send l).
Proof. intros P1 P2 HP. rewrite /send. by setoid_rewrite HP. Qed. Proof. (* TODO: This really ought to be doable by just calling a tactic.
It is just application of already registered congruence lemmas. *)
intros P1 P2 HP. rewrite /send. by setoid_rewrite HP. Qed.
Definition recv (l : loc) (R : iProp) : iProp := Definition recv (l : loc) (R : iProp) : iProp :=
(∃ γ P Q i, barrier_ctx γ l P ★ sts_ownS γ (i_states i) {[ Change i ]} ★ (∃ γ P Q i, barrier_ctx γ l P ★ sts_ownS γ (i_states i) {[ Change i ]} ★
......
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