Skip to content
Snippets Groups Projects
Commit 807bed4b authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Ralf Jung
Browse files

linebreaks

parent da9205f9
No related branches found
No related tags found
1 merge request!427make solve_ndisj work on goals of the form 'X1 ∪ X2 ## Y'
Pipeline #74817 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
Showing
with 4 additions and 2 deletions
stdpp/namespaces.v
+ 4
− 2
View file @ 807bed4b
...@@ -103,9 +103,11 @@ Global Hint Resolve coPset_disjoint_empty_l : ndisj. ...@@ -103,9 +103,11 @@ Global Hint Resolve coPset_disjoint_empty_l : ndisj.
Local Definition coPset_disjoint_empty_r := disjoint_empty_r (C:=coPset). Local Definition coPset_disjoint_empty_r := disjoint_empty_r (C:=coPset).
Global Hint Resolve coPset_disjoint_empty_r : ndisj. Global Hint Resolve coPset_disjoint_empty_r : ndisj.
(** If-and-only-if rules for ∪ on the left/right. *) (** If-and-only-if rules for ∪ on the left/right. *)
Local Definition coPset_disjoint_union_l X1 X2 Y := proj2 (disjoint_union_l (C:=coPset) X1 X2 Y). Local Definition coPset_disjoint_union_l X1 X2 Y :=
proj2 (disjoint_union_l (C:=coPset) X1 X2 Y).
Global Hint Resolve coPset_disjoint_union_l : ndisj. Global Hint Resolve coPset_disjoint_union_l : ndisj.
Local Definition coPset_disjoint_union_r X Y1 Y2 := proj2 (disjoint_union_r (C:=coPset) X Y1 Y2). Local Definition coPset_disjoint_union_r X Y1 Y2 :=
proj2 (disjoint_union_r (C:=coPset) X Y1 Y2).
Global Hint Resolve coPset_disjoint_union_r : ndisj. Global Hint Resolve coPset_disjoint_union_r : ndisj.
(** We prefer ∖ on the left of ## (for the [disjoint_difference] lemmas to (** We prefer ∖ on the left of ## (for the [disjoint_difference] lemmas to
apply), so try moving it there. *) apply), so try moving it there. *)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment