Commit 8da58b7f authored by Ralf Jung's avatar Ralf Jung

linebreaks for readability

parent 6d15d440
...@@ -306,7 +306,9 @@ Lemma insert_op m1 m2 i x y : ...@@ -306,7 +306,9 @@ Lemma insert_op m1 m2 i x y :
Proof. by rewrite (insert_merge () m1 m2 i (x y) x y). Qed. Proof. by rewrite (insert_merge () m1 m2 i (x y) x y). Qed.
Lemma insert_updateP (P : A Prop) (Q : gmap K A Prop) m i x : Lemma insert_updateP (P : A Prop) (Q : gmap K A Prop) m i x :
x ~~>: P ( y, P y Q (<[i:=y]>m)) <[i:=x]>m ~~>: Q. x ~~>: P
( y, P y Q (<[i:=y]>m))
<[i:=x]>m ~~>: Q.
Proof. Proof.
intros Hx%option_updateP' HP; apply cmra_total_updateP=> n mf Hm. intros Hx%option_updateP' HP; apply cmra_total_updateP=> n mf Hm.
destruct (Hx n (Some (mf !! i))) as ([y|]&?&?); try done. destruct (Hx n (Some (mf !! i))) as ([y|]&?&?); try done.
......
...@@ -134,7 +134,8 @@ Section gset_disj. ...@@ -134,7 +134,8 @@ Section gset_disj.
Lemma gset_disj_alloc_updateP_strong P (Q : gset_disj K Prop) X : Lemma gset_disj_alloc_updateP_strong P (Q : gset_disj K Prop) X :
( Y, X Y j, j Y P j) ( Y, X Y j, j Y P j)
( i, i X P i Q (GSet ({[i]} X))) GSet X ~~>: Q. ( i, i X P i Q (GSet ({[i]} X)))
GSet X ~~>: Q.
Proof. Proof.
intros Hfresh HQ. intros Hfresh HQ.
apply cmra_discrete_updateP=> ? /gset_disj_valid_inv_l [Y [->?]]. apply cmra_discrete_updateP=> ? /gset_disj_valid_inv_l [Y [->?]].
......
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