Commit 71bce7f8 authored by Ralf Jung's avatar Ralf Jung
Browse files

rename map_union_subseteq_l_alt → map_union_subseteq_l' (and likewise for _r)

parent c95596b7
Pipeline #50766 passed with stage
in 4 minutes and 45 seconds
......@@ -116,6 +116,9 @@ API-breaking change is listed.
- Swap names of `curry`/`uncurry`, `curry3`/`uncurry3`, `curry4`/`uncurry4`,
`gmap_curry`/`gmap_uncurry`, and `hcurry`/`huncurry` to be consistent with
Haskell and friends.
- Rename `map_union_subseteq_l_alt``map_union_subseteq_l'` and
`map_union_subseteq_r_alt``map_union_subseteq_r'` to be consistent with
`or_intro_{l,r}'`.
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
......@@ -156,6 +159,8 @@ s/\bgmap_uncurry_non_empty\b/gmap_curry_non_empty/g
s/\bgmap_uncurry_curry_non_empty\b/gmap_curry_uncurry_non_empty/g
s/\bhcurry_uncurry\b/huncurry_curry/g
s/\blookup_gmap_uncurry_None\b/lookup_gmap_curry_None/g
# map_union_subseteq
s/\bmap_union_subseteq_(r|l)_alt\b/map_union_subseteq_\1'/g
' $(find theories -name "*.v")
```
......
......@@ -2039,9 +2039,9 @@ Lemma map_union_subseteq_r {A} (m1 m2 : M A) : m1 ##ₘ m2 → m2 ⊆ m1 ∪ m2.
Proof.
intros. rewrite map_union_comm by done. by apply map_union_subseteq_l.
Qed.
Lemma map_union_subseteq_l_alt {A} (m1 m2 m3 : M A) : m1 m2 m1 m2 m3.
Lemma map_union_subseteq_l' {A} (m1 m2 m3 : M A) : m1 m2 m1 m2 m3.
Proof. intros. trans m2; auto using map_union_subseteq_l. Qed.
Lemma map_union_subseteq_r_alt {A} (m1 m2 m3 : M A) :
Lemma map_union_subseteq_r' {A} (m1 m2 m3 : M A) :
m2 ## m3 m1 m3 m1 m2 m3.
Proof. intros. trans m3; auto using map_union_subseteq_r. Qed.
Lemma map_union_mono_l {A} (m1 m2 m3 : M A) : m1 m2 m3 m1 m3 m2.
......
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