Commit 581e709f by Robbert Krebbers

### Make ∖ left associative.

parent 64bb0481
 ... @@ -590,7 +590,7 @@ Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : C_scope. ... @@ -590,7 +590,7 @@ Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : C_scope. Class Difference A := difference: A → A → A. Class Difference A := difference: A → A → A. Instance: Params (@difference) 2. Instance: Params (@difference) 2. Infix "∖" := difference (at level 40) : C_scope. Infix "∖" := difference (at level 40, left associativity) : C_scope. Notation "(∖)" := difference (only parsing) : C_scope. Notation "(∖)" := difference (only parsing) : C_scope. Notation "( x ∖)" := (difference x) (only parsing) : C_scope. Notation "( x ∖)" := (difference x) (only parsing) : C_scope. Notation "(∖ x )" := (λ y, difference y x) (only parsing) : C_scope. Notation "(∖ x )" := (λ y, difference y x) (only parsing) : C_scope. ... ...
 ... @@ -77,7 +77,7 @@ Section ndisjoint. ... @@ -77,7 +77,7 @@ Section ndisjoint. End ndisjoint. End ndisjoint. (* The hope is that registering these will suffice to solve most goals (* The hope is that registering these will suffice to solve most goals of the form [N1 ⊥ N2] and those of the form [((N1 ⊆ E ∖ N2) ∖ ..) ∖ Nn]. *) of the form [N1 ⊥ N2] and those of the form [N1 ⊆ E ∖ N2 ∖ .. ∖ Nn]. *) Hint Resolve ndisj_subseteq_difference : ndisj. Hint Resolve ndisj_subseteq_difference : ndisj. Hint Extern 0 (_ ⊥ _) => apply ndot_ne_disjoint; congruence : ndisj. Hint Extern 0 (_ ⊥ _) => apply ndot_ne_disjoint; congruence : ndisj. Hint Resolve ndot_preserve_disjoint_l : ndisj. Hint Resolve ndot_preserve_disjoint_l : ndisj. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!