Commit a70caa4b authored by Robbert Krebbers's avatar Robbert Krebbers

All multiset elements are cancelable.

parent 465dd9f4
......@@ -50,6 +50,11 @@ Section gmultiset.
Proof. split. done. intros X. by rewrite gmultiset_op_union left_id_L. done. Qed.
Canonical Structure gmultisetUR := UcmraT (gmultiset K) gmultiset_ucmra_mixin.
Global Instance gmultiset_cancelable X : Cancelable X.
Proof.
apply: discrete_cancelable=> Y Z _ ?. fold_leibniz. by apply (inj (X )).
Qed.
Lemma gmultiset_opM X mY : X ? mY = X from_option id mY.
Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
......@@ -71,7 +76,6 @@ Section gmultiset.
repeat (rewrite multiplicity_difference || rewrite multiplicity_union).
omega.
Qed.
End gmultiset.
Arguments gmultisetC _ {_ _}.
......
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