...

Commits (3)
This diff is collapsed.
 ... ... @@ -191,7 +191,7 @@ Proof. Qed. Instance coPset_elem_of_dec : RelDecision (∈@{coPset}). Proof. solve_decision. Defined. Proof. unfold elem_of. solve_decision. Defined. Instance coPset_equiv_dec : RelDecision (≡@{coPset}). Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined. Instance mapset_disjoint_dec : RelDecision (##@{coPset}). ... ...
 ... ... @@ -233,7 +233,7 @@ Proof. Qed. Global Instance map_subseteq_po : PartialOrder (⊆@{M A}). Proof. split; [apply _|]. split; [apply map_included_preorder, _|]. intros m1 m2; rewrite !map_subseteq_spec. intros; apply map_eq; intros i; apply option_eq; naive_solver. Qed. ... ... @@ -1534,8 +1534,10 @@ Qed. End union_with. (** ** Properties of the [union] operation *) Global Instance: LeftId (=@{M A}) ∅ (∪) := _. Global Instance: RightId (=@{M A}) ∅ (∪) := _. Global Instance: LeftId (=@{M A}) ∅ (∪). Proof. unfold union; apply _. Qed. Global Instance: RightId (=@{M A}) ∅ (∪). Proof. unfold union; apply _. Qed. Global Instance: Assoc (=@{M A}) (∪). Proof. intros A m1 m2 m3. unfold union, map_union, union_with, map_union_with. ... ...
 ... ... @@ -130,8 +130,4 @@ Proof. Qed. End mapset. (** [mapset_elem_of] internally contains an equality; make sure that tactics do not unfold it and try to unify [∈] against goals with [=]. *) Opaque mapset_elem_of. Arguments mapset_eq_dec : simpl never.