From e8359b861d167c645ca5406233dabfa2f81db875 Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Tue, 1 Aug 2023 23:27:32 -0500
Subject: [PATCH 1/8] =?UTF-8?q?Add=20some=20`=5F=E2=88=B7=CA=B3=5F`=20prop?=
 =?UTF-8?q?erties=20to=20`Data.Vec.Properties`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Vec/Properties.agda | 35 ++++++++++++++++++++++++++++++++++-
 1 file changed, 34 insertions(+), 1 deletion(-)

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index c7719eedf1..ee808bcce9 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -399,7 +399,7 @@ cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (suc-injective eq) xs)
 subst-is-cast : (eq : m ≡ n) (xs : Vec A m) → subst (Vec A) eq xs ≡ cast eq xs
 subst-is-cast refl xs = sym (cast-is-id refl xs)
 
-cast-trans : .(eq₁ : m ≡ n) (eq₂ : n ≡ o) (xs : Vec A m) →
+cast-trans : .(eq₁ : m ≡ n) .(eq₂ : n ≡ o) (xs : Vec A m) →
              cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
 cast-trans {m = zero}  {n = zero}  {o = zero}  eq₁ eq₂ [] = refl
 cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (x ∷ xs) =
@@ -839,6 +839,12 @@ map-is-foldr f = foldr-universal (Vec _) (λ x ys → f x ∷ ys) (map f) refl (
 ------------------------------------------------------------------------
 -- _∷ʳ_
 
+-- snoc is snoc
+
+unfold-∷ʳ : ∀ .(eq : n + 1 ≡ suc n) x (xs : Vec A n) → cast eq (xs ++ x ∷ []) ≡ xs ∷ʳ x
+unfold-∷ʳ eq x []       = refl
+unfold-∷ʳ eq x (y ∷ xs) = cong (y ∷_) (unfold-∷ʳ (cong pred eq) x xs)
+
 ∷ʳ-injective : ∀ (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y
 ∷ʳ-injective []       []        refl = (refl , refl)
 ∷ʳ-injective (x ∷ xs) (y  ∷ ys) eq   with ∷-injective eq
@@ -860,12 +866,39 @@ foldr-∷ʳ : ∀ (B : ℕ → Set b) (f : FoldrOp A B) {e} y (ys : Vec A n) →
 foldr-∷ʳ B f y []       = refl
 foldr-∷ʳ B f y (x ∷ xs) = cong (f x) (foldr-∷ʳ B f y xs)
 
+-- init, last and _∷ʳ_
+
+init-∷ʳ : ∀ x (xs : Vec A n) → init (xs ∷ʳ x) ≡ xs
+init-∷ʳ x xs with xs ∷ʳ x in eq
+init-∷ʳ x xs | xs* with initLast xs*
+init-∷ʳ x xs | .(xs′ ∷ʳ x′) | xs′ , x′ , refl = sym (proj₁ (∷ʳ-injective xs xs′ eq))
+
+last-∷ʳ : ∀ x (xs : Vec A n) → last (xs ∷ʳ x) ≡ x
+last-∷ʳ x xs with xs ∷ʳ x in eq
+last-∷ʳ x xs | xs* with initLast xs*
+last-∷ʳ x xs | .(xs′ ∷ʳ x′) | xs′ , x′ , refl = sym (proj₂ (∷ʳ-injective xs xs′ eq))
+
 -- map and _∷ʳ_
 
 map-∷ʳ : ∀ (f : A → B) x (xs : Vec A n) → map f (xs ∷ʳ x) ≡ map f xs ∷ʳ f x
 map-∷ʳ f x []       = refl
 map-∷ʳ f x (y ∷ xs) = cong (f y ∷_) (map-∷ʳ f x xs)
 
+-- cast and _∷ʳ_
+
+cast-∷ʳ : ∀ .(eq : suc n ≡ suc m) x (xs : Vec A n) →
+          cast eq (xs ∷ʳ x) ≡ (cast (cong pred eq) xs) ∷ʳ x
+cast-∷ʳ {m = zero}  eq x []       = refl
+cast-∷ʳ {m = suc m} eq x (y ∷ xs) = cong (y ∷_) (cast-∷ʳ (cong pred eq) x xs)
+
+-- _++_ and _∷ʳ_
+
+++-∷ʳ : ∀ .(eq : suc (n + m) ≡ n + suc m) z (xs : Vec A n) (ys : Vec A m) →
+        (cast eq ((xs ++ ys) ∷ʳ z)) ≡ xs ++ (ys ∷ʳ z)
+++-∷ʳ {n = zero}  eq z []       []       = refl
+++-∷ʳ {n = zero}  eq z []       (y ∷ ys) = cong (y ∷_) (++-∷ʳ refl z [] ys)
+++-∷ʳ {n = suc n} eq z (x ∷ xs) ys       = cong (x ∷_) (++-∷ʳ (cong pred eq) z xs ys)
+
 ------------------------------------------------------------------------
 -- reverse
 

From e83d525427da282c3289cbf95020d283a52beb9e Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Wed, 2 Aug 2023 12:17:31 -0500
Subject: [PATCH 2/8] PR feedback: direct definition of `init` and `last`

---
 src/Data/Vec/Base.agda       |  8 ++++----
 src/Data/Vec/Properties.agda | 10 ++++------
 2 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 9f6d86b792..9891c347ea 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -345,12 +345,12 @@ initLast {n = suc n} (x ∷ xs) with initLast xs
 ... | (ys , y , refl) = (x ∷ ys , y , refl)
 
 init : Vec A (1 + n) → Vec A n
-init xs with initLast xs
-... | (ys , y , refl) = ys
+init {n = zero}  (x ∷ []) = []
+init {n = suc n} (x ∷ xs) = x ∷ init xs
 
 last : Vec A (1 + n) → A
-last xs with initLast xs
-... | (ys , y , refl) = y
+last {n = zero}  (x ∷ []) = x
+last {n = suc n} (x ∷ xs) = last xs
 
 ------------------------------------------------------------------------
 -- Other operations
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index ee808bcce9..f56d50e41b 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -869,14 +869,12 @@ foldr-∷ʳ B f y (x ∷ xs) = cong (f x) (foldr-∷ʳ B f y xs)
 -- init, last and _∷ʳ_
 
 init-∷ʳ : ∀ x (xs : Vec A n) → init (xs ∷ʳ x) ≡ xs
-init-∷ʳ x xs with xs ∷ʳ x in eq
-init-∷ʳ x xs | xs* with initLast xs*
-init-∷ʳ x xs | .(xs′ ∷ʳ x′) | xs′ , x′ , refl = sym (proj₁ (∷ʳ-injective xs xs′ eq))
+init-∷ʳ x []       = refl
+init-∷ʳ x (y ∷ xs) = cong (y ∷_) (init-∷ʳ x xs)
 
 last-∷ʳ : ∀ x (xs : Vec A n) → last (xs ∷ʳ x) ≡ x
-last-∷ʳ x xs with xs ∷ʳ x in eq
-last-∷ʳ x xs | xs* with initLast xs*
-last-∷ʳ x xs | .(xs′ ∷ʳ x′) | xs′ , x′ , refl = sym (proj₂ (∷ʳ-injective xs xs′ eq))
+last-∷ʳ x []       = refl
+last-∷ʳ x (y ∷ xs) = last-∷ʳ x xs
 
 -- map and _∷ʳ_
 

From dd4e917b7e4fc3829b467c1cffff7f3a7c041e10 Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Fri, 11 Aug 2023 00:07:54 -0500
Subject: [PATCH 3/8] PR feedback: edit CHANGELOG and adjust init, last

---
 CHANGELOG.md           | 8 ++++++++
 src/Data/Vec/Base.agda | 4 ++--
 2 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3818f1a6f7..decf82a8b7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -858,6 +858,8 @@ Non-backwards compatible changes
 
 * In `Data.Sum.Base` the definitions `fromDec` and `toDec` have been moved to `Data.Sum`.
 
+* In `Data.Vec.Base`: the definitions `init` and `last` have been replaced by an inductive definition.
+
 * In `Codata.Guarded.Stream` the following functions have been modified to have simpler definitions:
   * `cycle`
   * `interleave⁺`
@@ -2610,6 +2612,12 @@ Other minor changes
   ∷ʳ-injectiveˡ : xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys
   ∷ʳ-injectiveʳ : xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y
 
+  unfold-∷ʳ : cast eq (xs ++ x ∷ []) ≡ xs ∷ʳ x
+  init-∷ʳ   : init (xs ∷ʳ x) ≡ xs
+  last-∷ʳ   : last (xs ∷ʳ x) ≡ x
+  cast-∷ʳ   : cast eq (xs ∷ʳ x) ≡ (cast (cong pred eq) xs) ∷ʳ x
+  ++-∷ʳ     : (cast eq ((xs ++ ys) ∷ʳ z)) ≡ xs ++ (ys ∷ʳ z)
+
   reverse-∷          : reverse (x ∷ xs) ≡ reverse xs ∷ʳ x
   reverse-involutive : Involutive _≡_ reverse
   reverse-reverse    : reverse xs ≡ ys → reverse ys ≡ xs
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 9891c347ea..6bdcc79abd 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -345,11 +345,11 @@ initLast {n = suc n} (x ∷ xs) with initLast xs
 ... | (ys , y , refl) = (x ∷ ys , y , refl)
 
 init : Vec A (1 + n) → Vec A n
-init {n = zero}  (x ∷ []) = []
+init {n = zero}  (x ∷ xs) = []
 init {n = suc n} (x ∷ xs) = x ∷ init xs
 
 last : Vec A (1 + n) → A
-last {n = zero}  (x ∷ []) = x
+last {n = zero}  (x ∷ xs) = x
 last {n = suc n} (x ∷ xs) = last xs
 
 ------------------------------------------------------------------------

From e1fedbd8bb6f6a5bd51e326ed48ae044bced7bd1 Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Sat, 12 Aug 2023 19:07:57 -0500
Subject: [PATCH 4/8] PR feedback: edit CHANGELOG and init/last matching

---
 CHANGELOG.md           | 3 ++-
 src/Data/Vec/Base.agda | 6 +++---
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index decf82a8b7..a0c9eaaa39 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -858,7 +858,8 @@ Non-backwards compatible changes
 
 * In `Data.Sum.Base` the definitions `fromDec` and `toDec` have been moved to `Data.Sum`.
 
-* In `Data.Vec.Base`: the definitions `init` and `last` have been replaced by an inductive definition.
+* In `Data.Vec.Base`: the definitions `init` and `last` have been changed from the `initLast`
+  view-derived implementation to direct recursive definitions.
 
 * In `Codata.Guarded.Stream` the following functions have been modified to have simpler definitions:
   * `cycle`
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 6bdcc79abd..0bf095eaa1 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -345,12 +345,12 @@ initLast {n = suc n} (x ∷ xs) with initLast xs
 ... | (ys , y , refl) = (x ∷ ys , y , refl)
 
 init : Vec A (1 + n) → Vec A n
-init {n = zero}  (x ∷ xs) = []
+init {n = zero}  (x ∷ _)  = []
 init {n = suc n} (x ∷ xs) = x ∷ init xs
 
 last : Vec A (1 + n) → A
-last {n = zero}  (x ∷ xs) = x
-last {n = suc n} (x ∷ xs) = last xs
+last {n = zero}  (x ∷ _)  = x
+last {n = suc n} (_ ∷ xs) = last xs
 
 ------------------------------------------------------------------------
 -- Other operations

From 5cdcc146466e2df2a717a7138ed1df87912db0c8 Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Sat, 12 Aug 2023 19:10:01 -0500
Subject: [PATCH 5/8] =?UTF-8?q?PR=20feedback:=20flip=20the=20equality=20of?=
 =?UTF-8?q?=20unfold-=E2=88=B7=CA=B3?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                 | 2 +-
 src/Data/Vec/Properties.agda | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a0c9eaaa39..d1475de21a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2613,7 +2613,7 @@ Other minor changes
   ∷ʳ-injectiveˡ : xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys
   ∷ʳ-injectiveʳ : xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y
 
-  unfold-∷ʳ : cast eq (xs ++ x ∷ []) ≡ xs ∷ʳ x
+  unfold-∷ʳ : cast eq (xs ∷ʳ x) ≡ xs ++ [ x ]
   init-∷ʳ   : init (xs ∷ʳ x) ≡ xs
   last-∷ʳ   : last (xs ∷ʳ x) ≡ x
   cast-∷ʳ   : cast eq (xs ∷ʳ x) ≡ (cast (cong pred eq) xs) ∷ʳ x
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index f56d50e41b..1c7c3ba3e9 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -841,7 +841,7 @@ map-is-foldr f = foldr-universal (Vec _) (λ x ys → f x ∷ ys) (map f) refl (
 
 -- snoc is snoc
 
-unfold-∷ʳ : ∀ .(eq : n + 1 ≡ suc n) x (xs : Vec A n) → cast eq (xs ++ x ∷ []) ≡ xs ∷ʳ x
+unfold-∷ʳ : ∀ .(eq : suc n ≡ n + 1) x (xs : Vec A n) → cast eq (xs ∷ʳ x) ≡ xs ++ [ x ]
 unfold-∷ʳ eq x []       = refl
 unfold-∷ʳ eq x (y ∷ xs) = cong (y ∷_) (unfold-∷ʳ (cong pred eq) x xs)
 

From 6f76b4b631430df725f6fd1025c157f56a85fb36 Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Sat, 12 Aug 2023 19:55:44 -0500
Subject: [PATCH 6/8] =?UTF-8?q?Fix=20the=20index=20order=20of=20++-?=
 =?UTF-8?q?=E2=88=B7=CA=B3=20per=20the=20style=20guide?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                 |  2 +-
 src/Data/Vec/Properties.agda | 10 +++++-----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d1475de21a..09a58e90fa 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2617,7 +2617,7 @@ Other minor changes
   init-∷ʳ   : init (xs ∷ʳ x) ≡ xs
   last-∷ʳ   : last (xs ∷ʳ x) ≡ x
   cast-∷ʳ   : cast eq (xs ∷ʳ x) ≡ (cast (cong pred eq) xs) ∷ʳ x
-  ++-∷ʳ     : (cast eq ((xs ++ ys) ∷ʳ z)) ≡ xs ++ (ys ∷ʳ z)
+  ++-∷ʳ     : cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
 
   reverse-∷          : reverse (x ∷ xs) ≡ reverse xs ∷ʳ x
   reverse-involutive : Involutive _≡_ reverse
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 1c7c3ba3e9..cb943c9f28 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -891,11 +891,11 @@ cast-∷ʳ {m = suc m} eq x (y ∷ xs) = cong (y ∷_) (cast-∷ʳ (cong pred eq
 
 -- _++_ and _∷ʳ_
 
-++-∷ʳ : ∀ .(eq : suc (n + m) ≡ n + suc m) z (xs : Vec A n) (ys : Vec A m) →
-        (cast eq ((xs ++ ys) ∷ʳ z)) ≡ xs ++ (ys ∷ʳ z)
-++-∷ʳ {n = zero}  eq z []       []       = refl
-++-∷ʳ {n = zero}  eq z []       (y ∷ ys) = cong (y ∷_) (++-∷ʳ refl z [] ys)
-++-∷ʳ {n = suc n} eq z (x ∷ xs) ys       = cong (x ∷_) (++-∷ʳ (cong pred eq) z xs ys)
+++-∷ʳ : ∀ .(eq : suc (m + n) ≡ m + suc n) z (xs : Vec A m) (ys : Vec A n) →
+        cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
+++-∷ʳ {m = zero}  eq z []       []       = refl
+++-∷ʳ {m = zero}  eq z []       (y ∷ ys) = cong (y ∷_) (++-∷ʳ refl z [] ys)
+++-∷ʳ {m = suc m} eq z (x ∷ xs) ys       = cong (x ∷_) (++-∷ʳ (cong pred eq) z xs ys)
 
 ------------------------------------------------------------------------
 -- reverse

From bb98e1999a6547f94d6d3d4e06ef68390bd12612 Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Sun, 13 Aug 2023 11:34:06 -0500
Subject: [PATCH 7/8] =?UTF-8?q?Rename=20`Data.List.Properties.=CA=B3++-++`?=
 =?UTF-8?q?=20to=20`++-=CA=B3++`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                  |  2 ++
 src/Data/List/Properties.agda | 16 +++++++++++-----
 2 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 09a58e90fa..feb4e8b75e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1242,6 +1242,8 @@ Deprecated names
 
   zipWith-identityˡ  ↦  zipWith-zeroˡ
   zipWith-identityʳ  ↦  zipWith-zeroʳ
+
+  ʳ++-++  ↦  ++-ʳ++
   ```
 
 * In `Data.List.NonEmpty.Properties`:
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index ca5ffe27f2..6e47de4a86 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -983,11 +983,11 @@ module _ {P : Pred A p} (P? : Decidable P) where
 
 -- Reverse-append of append is reverse-append after reverse-append.
 
-ʳ++-++ : ∀ (xs {ys zs} : List A) → (xs ++ ys) ʳ++ zs ≡ ys ʳ++ xs ʳ++ zs
-ʳ++-++ [] = refl
-ʳ++-++ (x ∷ xs) {ys} {zs} = begin
+++-ʳ++ : ∀ (xs {ys zs} : List A) → (xs ++ ys) ʳ++ zs ≡ ys ʳ++ xs ʳ++ zs
+++-ʳ++ [] = refl
+++-ʳ++ (x ∷ xs) {ys} {zs} = begin
   (x ∷ xs ++ ys) ʳ++ zs   ≡⟨⟩
-  (xs ++ ys) ʳ++ x ∷ zs   ≡⟨ ʳ++-++ xs ⟩
+  (xs ++ ys) ʳ++ x ∷ zs   ≡⟨ ++-ʳ++ xs ⟩
   ys ʳ++ xs ʳ++ x ∷ zs    ≡⟨⟩
   ys ʳ++ (x ∷ xs) ʳ++ zs  ∎
 
@@ -1063,7 +1063,7 @@ reverse-++ : (xs ys : List A) →
                      reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
 reverse-++ xs ys = begin
   reverse (xs ++ ys)         ≡⟨⟩
-  (xs ++ ys) ʳ++ []          ≡⟨ ʳ++-++ xs ⟩
+  (xs ++ ys) ʳ++ []          ≡⟨ ++-ʳ++ xs ⟩
   ys ʳ++ xs ʳ++ []           ≡⟨⟩
   ys ʳ++ reverse xs          ≡⟨ ʳ++-defn ys ⟩
   reverse ys ++ reverse xs   ∎
@@ -1202,3 +1202,9 @@ zipWith-identityʳ = zipWith-zeroʳ
 "Warning: zipWith-identityʳ was deprecated in v2.0.
 Please use zipWith-zeroʳ instead."
 #-}
+
+ʳ++-++ = ++-ʳ++
+{-# WARNING_ON_USAGE ʳ++-++
+"Warning: ʳ++-++ was deprecated in v2.0.
+Please use ++-ʳ++ instead."
+#-}

From 4e2d46ddc14480001cce7fdbe93a090413731b6a Mon Sep 17 00:00:00 2001
From: shhyou <shu-hung.you@eecs.northwestern.edu>
Date: Wed, 30 Aug 2023 16:51:09 -0500
Subject: [PATCH 8/8] try to resolve conflict

---
 CHANGELOG.md                  |  4 ++++
 README/Data/List.agda         |  2 +-
 src/Data/List/Properties.agda | 14 ++++++++++----
 src/Data/Vec/Properties.agda  | 14 ++++++++++----
 4 files changed, 25 insertions(+), 9 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index feb4e8b75e..d2cee50692 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1244,6 +1244,8 @@ Deprecated names
   zipWith-identityʳ  ↦  zipWith-zeroʳ
 
   ʳ++-++  ↦  ++-ʳ++
+
+  take++drop ↦ take++drop≡id
   ```
 
 * In `Data.List.NonEmpty.Properties`:
@@ -1399,6 +1401,8 @@ Deprecated names
   []≔-++-raise    ↦ []≔-++-↑ʳ
   idIsFold        ↦ id-is-foldr
   sum-++-commute  ↦ sum-++
+
+  take-drop-id ↦ take++drop≡id
   ```
   and the type of the proof `zipWith-comm` has been generalised from:
   ```
diff --git a/README/Data/List.agda b/README/Data/List.agda
index 6cb8bba0b1..2c284daa78 100644
--- a/README/Data/List.agda
+++ b/README/Data/List.agda
@@ -48,7 +48,7 @@ lem₅ = refl
 open import Data.List.Properties
 
 lem₆ : ∀ n (xs : List ℕ) → take n xs ++ drop n xs ≡ xs
-lem₆ = take++drop
+lem₆ = take++drop≡id
 
 lem₇ : ∀ (xs : List ℕ) → reverse (reverse xs) ≡ xs
 lem₇ = reverse-involutive
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 6e47de4a86..d672f8f687 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -809,10 +809,10 @@ drop-[] : ∀ m → drop {A = A} m [] ≡ []
 drop-[] zero = refl
 drop-[] (suc m) = refl
 
-take++drop : ∀ n (xs : List A) → take n xs ++ drop n xs ≡ xs
-take++drop zero    xs       = refl
-take++drop (suc n) []       = refl
-take++drop (suc n) (x ∷ xs) = cong (x ∷_) (take++drop n xs)
+take++drop≡id : ∀ n (xs : List A) → take n xs ++ drop n xs ≡ xs
+take++drop≡id zero    xs       = refl
+take++drop≡id (suc n) []       = refl
+take++drop≡id (suc n) (x ∷ xs) = cong (x ∷_) (take++drop≡id n xs)
 
 drop-take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in
            drop m (take (suc m) xs) ≡ [ lookup xs i ]
@@ -1208,3 +1208,9 @@ Please use zipWith-zeroʳ instead."
 "Warning: ʳ++-++ was deprecated in v2.0.
 Please use ++-ʳ++ instead."
 #-}
+
+take++drop = take++drop≡id
+{-# WARNING_ON_USAGE take++drop
+"Warning: take++drop was deprecated in v2.0.
+Please use take++drop≡id instead."
+#-}
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index cb943c9f28..bbf716143f 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -139,15 +139,15 @@ drop-distr-map f (suc m) (x ∷ xs) = begin
 ------------------------------------------------------------------------
 -- take and drop together
 
-take-drop-id : ∀ (m : ℕ) (x : Vec A (m + n)) → take m x ++ drop m x ≡ x
-take-drop-id zero x = refl
-take-drop-id (suc m) (x ∷ xs) = begin
+take++drop≡id : ∀ (m : ℕ) (x : Vec A (m + n)) → take m x ++ drop m x ≡ x
+take++drop≡id zero x = refl
+take++drop≡id (suc m) (x ∷ xs) = begin
     take (suc m) (x ∷ xs) ++ drop (suc m) (x ∷ xs)
   ≡⟨ cong₂ _++_ (unfold-take m x xs) (unfold-drop m x xs) ⟩
     (x ∷ take m xs) ++ (drop m xs)
   ≡⟨⟩
     x ∷ (take m xs ++ drop m xs)
-  ≡⟨ cong (x ∷_) (take-drop-id m xs) ⟩
+  ≡⟨ cong (x ∷_) (take++drop≡id m xs) ⟩
     x ∷ xs
   ∎
 
@@ -1187,3 +1187,9 @@ sum-++-commute = sum-++
 "Warning: sum-++-commute was deprecated in v2.0.
 Please use sum-++ instead."
 #-}
+
+take-drop-id = take++drop≡id
+{-# WARNING_ON_USAGE take-drop-id
+"Warning: take-drop-id was deprecated in v2.0.
+Please use take++drop≡id instead."
+#-}