Rename drop-fusion and drop-drop-fusion to drop-drop

Author: Saransh-cpp

CHANGELOG.md

@@ -1080,12 +1080,14 @@ Deprecated names
   ```agda
   map-identity  ↦  map-id
   map-fusion    ↦  map-∘
+  drop-fusion   ↦  drop-drop
   ```
 
 * In `Codata.Sized.Colist.Properties`:
   ```agda
-  map-identity   ↦  map-id
-  map-map-fusion  ↦  map-∘
+  map-identity      ↦  map-id
+  map-map-fusion    ↦  map-∘
+  drop-drop-fusion  ↦  drop-drop
   ```
 
 * In `Codata.Sized.Covec.Properties`:

src/Codata/Guarded/Stream/Properties.agda

@@ -268,9 +268,9 @@ take-zipWith (suc n) f as bs =
 ------------------------------------------------------------------------
 -- Properties of drop
 
-drop-fusion : ∀ m n (as : Stream A) → drop n (drop m as) ≡ drop (m + n) as
-drop-fusion zero    n as = P.refl
-drop-fusion (suc m) n as = drop-fusion m n (as .tail)
+drop-drop : ∀ m n (as : Stream A) → drop n (drop m as) ≡ drop (m + n) as
+drop-drop zero    n as = P.refl
+drop-drop (suc m) n as = drop-drop m n (as .tail)
 
 drop-zipWith : ∀ n (f : A → B → C) as bs →
                drop n (zipWith f as bs) ≡ zipWith f (drop n as) (drop n bs)
@@ -331,3 +331,9 @@ map-fusion = map-∘
 "Warning: map-fusion was deprecated in v2.0.
 Please use map-∘ instead."
 #-}
+
+drop-fusion = drop-drop
+{-# WARNING_ON_USAGE drop-fusion
+"Warning: drop-fusion was deprecated in v2.0.
+Please use drop-drop instead."
+#-}

src/Codata/Sized/Colist/Properties.agda

@@ -197,11 +197,11 @@ drop-nil : ∀ m → i ⊢ drop {A = A} m [] ≈ []
 drop-nil zero    = []
 drop-nil (suc m) = []
 
-drop-drop-fusion : ∀ m n (as : Colist A ∞) →
+drop-drop : ∀ m n (as : Colist A ∞) →
                    i ⊢ drop n (drop m as) ≈ drop (m ℕ.+ n) as
-drop-drop-fusion zero    n as       = refl
-drop-drop-fusion (suc m) n []       = drop-nil n
-drop-drop-fusion (suc m) n (a ∷ as) = drop-drop-fusion m n (as .force)
+drop-drop zero    n as       = refl
+drop-drop (suc m) n []       = drop-nil n
+drop-drop (suc m) n (a ∷ as) = drop-drop m n (as .force)
 
 map-drop : ∀ (f : A → B) m as → i ⊢ map f (drop m as) ≈ drop m (map f as)
 map-drop f zero    as       = refl
@@ -351,3 +351,9 @@ map-map-fusion = map-∘
 "Warning: map-map-fusion was deprecated in v2.0.
 Please use map-∘ instead."
 #-}
+
+drop-drop-fusion = drop-drop
+{-# WARNING_ON_USAGE drop-drop-fusion
+"Warning: drop-drop-fusion was deprecated in v2.0.
+Please use drop-drop instead."
+#-}