Commit 10edecb6 authored by Robbert Krebbers's avatar Robbert Krebbers

Notation `##@{A}`.

parent 210bf091
......@@ -866,6 +866,10 @@ Infix "##" := disjoint (at level 70) : stdpp_scope.
Notation "(##)" := disjoint (only parsing) : stdpp_scope.
Notation "( X ##.)" := (disjoint X) (only parsing) : stdpp_scope.
Notation "(.## X )" := (λ Y, Y ## X) (only parsing) : stdpp_scope.
Infix "##@{ A }" := (@disjoint A _) (at level 70, only parsing) : stdpp_scope.
Notation "(##@{ A } )" := (@disjoint A _) (only parsing) : stdpp_scope.
Infix "##*" := (Forall2 (##)) (at level 70) : stdpp_scope.
Notation "(##*)" := (Forall2 (##)) (only parsing) : stdpp_scope.
Infix "##**" := (Forall2 (##*)) (at level 70) : stdpp_scope.
......@@ -897,17 +901,19 @@ Class DisjointList A := disjoint_list : list A → Prop.
Hint Mode DisjointList ! : typeclass_instances.
Instance: Params (@disjoint_list) 2.
Notation "## Xs" := (disjoint_list Xs) (at level 20, format "## Xs") : stdpp_scope.
Notation "##@{ A } Xs" :=
(@disjoint_list A _ Xs) (at level 20, only parsing) : stdpp_scope.
Section disjoint_list.
Context `{Disjoint A, Union A, Empty A}.
Implicit Types X : A.
Inductive disjoint_list_default : DisjointList A :=
| disjoint_nil_2 : ## (@nil A)
| disjoint_nil_2 : ##@{A} []
| disjoint_cons_2 (X : A) (Xs : list A) : X ## Xs ## Xs ## (X :: Xs).
Global Existing Instance disjoint_list_default.
Lemma disjoint_list_nil : ## @nil A True.
Lemma disjoint_list_nil : ##@{A} [] True.
Proof. split; constructor. Qed.
Lemma disjoint_list_cons X Xs : ## (X :: Xs) X ## Xs ## Xs.
Proof. split. inversion_clear 1; auto. intros [??]. constructor; auto. Qed.
......
......@@ -194,7 +194,7 @@ Instance coPset_elem_of_dec : RelDecision (∈@{coPset}).
Proof. 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 (@disjoint coPset _).
Instance mapset_disjoint_dec : RelDecision (##@{coPset}).
Proof.
refine (λ X Y, cast_if (decide (X Y = )));
abstract (by rewrite disjoint_intersection_L).
......
......@@ -30,7 +30,7 @@ Section setoids_simple.
Proof. apply _. Qed.
Global Instance elem_of_proper : Proper ((=) ==> () ==> iff) (@{C}) | 5.
Proof. by intros x ? <- X Y. Qed.
Global Instance disjoint_proper: Proper (() ==> () ==> iff) (@disjoint C _).
Global Instance disjoint_proper: Proper (() ==> () ==> iff) (##@{C}).
Proof.
intros X1 X2 HX Y1 Y2 HY; apply forall_proper; intros x. by rewrite HX, HY.
Qed.
......@@ -407,7 +407,7 @@ Section simple_collection.
Lemma elem_of_disjoint X Y : X ## Y x, x X x Y False.
Proof. done. Qed.
Global Instance disjoint_sym : Symmetric (@disjoint C _).
Global Instance disjoint_sym : Symmetric (##@{C}).
Proof. intros X Y. set_solver. Qed.
Lemma disjoint_empty_l Y : ## Y.
Proof. set_solver. Qed.
......
......@@ -80,7 +80,7 @@ Section deciders.
Proof. refine (λ X1 X2, cast_if (decide (X1 = X2))); abstract (by fold_leibniz). Defined.
Global Instance mapset_elem_of_dec : RelDecision (@{mapset M}) | 1.
Proof. refine (λ x X, cast_if (decide (mapset_car X !! x = Some ()))); done. Defined.
Global Instance mapset_disjoint_dec : RelDecision (@disjoint (mapset M) _).
Global Instance mapset_disjoint_dec : RelDecision (##@{mapset M}).
Proof.
refine (λ X1 X2, cast_if (decide (X1 X2 = )));
abstract (by rewrite disjoint_intersection_L).
......
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