Commit b79eb4fe authored by Robbert Krebbers's avatar Robbert Krebbers

`Cancelable` instances for gmap/option.

parent 5e608261
......@@ -1395,6 +1395,10 @@ Section option.
by eapply (cmra_validN_le n); last lia.
- done.
Qed.
Global Instance option_cancelable (ma : option A) :
( a : A, IdFree a) ( a : A, Cancelable a) Cancelable ma.
Proof. destruct ma; apply _. Qed.
End option.
Arguments optionR : clear implicits.
......
......@@ -288,6 +288,12 @@ Proof.
- by rewrite lookup_singleton_ne // !(left_id None _).
Qed.
Global Instance gmap_cancelable (m : gmap K A) :
( x : A, IdFree x) ( x : A, Cancelable x) Cancelable m.
Proof.
intros ?? n m1 m2 ?? i. apply (cancelableN (m !! i)); by rewrite -!lookup_op.
Qed.
Lemma insert_op m1 m2 i x y :
<[i:=x y]>(m1 m2) = <[i:=x]>m1 <[i:=y]>m2.
Proof. by rewrite (insert_merge () m1 m2 i (x y) x y). Qed.
......
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