Deprecate Data.List.Relation.Unary.All.Properties.takeWhile⁻ (#2522)

* refactor: generalise type of `takeWhile⁻`

* deprecate rather than refactor

* refactor: generalise `takeWhile⁺`

* refactor: generalise `dropWhile⁻`

* roll back to simple deprecation PR

CHANGELOG.md

@@ -88,6 +88,11 @@ Deprecated names
   with a more informative type (see below).
   ```
 
+* In `Data.List.Relation.Unary.All.Properties`:
+  ```agda
+  takeWhile⁻  ↦  all-takeWhile
+  ```
+
 * In `Data.Vec.Properties`:
   ```agda
   ++-assoc _      ↦  ++-assoc-eqFree

src/Data/List/Relation/Unary/All/Properties.agda

@@ -43,13 +43,13 @@ open import Relation.Binary.Core using (REL)
 open import Relation.Binary.Bundles using (Setoid)
 import Relation.Binary.Definitions as B
 open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; cong; cong₂; _≗_)
+  using (_≡_; refl; sym; cong; cong₂; _≗_)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Decidable
   using (Dec; does; yes; no; _because_; ¬?; decidable-stable; dec-true)
 open import Relation.Unary
-  using (Decidable; Pred; Universal; ∁; _∩_; _⟨×⟩_) renaming (_⊆_ to _⋐_)
+  using (Decidable; Pred; ∁; _∩_; _⟨×⟩_) renaming (_⊆_ to _⋐_)
 open import Relation.Unary.Properties using (∁?)
 
 private
@@ -444,9 +444,9 @@ drop⁺ (suc n) (px ∷ pxs) = drop⁺ n pxs
 
 dropWhile⁺ : (Q? : Decidable Q) → All P xs → All P (dropWhile Q? xs)
 dropWhile⁺               Q? []         = []
-dropWhile⁺ {xs = x ∷ xs} Q? (px ∷ pxs) with does (Q? x)
+dropWhile⁺ {xs = x ∷ xs} Q? px∷pxs@(_ ∷ pxs) with does (Q? x)
 ... | true  = dropWhile⁺ Q? pxs
-... | false = px ∷ pxs
+... | false = px∷pxs
 
 dropWhile⁻ : (P? : Decidable P) → dropWhile P? xs ≡ [] → All P xs
 dropWhile⁻ {xs = []}     P? eq = []
@@ -477,12 +477,6 @@ takeWhile⁺ {xs = x ∷ xs} Q? (px ∷ pxs) with does (Q? x)
 ... | true  = px ∷ takeWhile⁺ Q? pxs
 ... | false = []
 
-takeWhile⁻ : (P? : Decidable P) → takeWhile P? xs ≡ xs → All P xs
-takeWhile⁻ {xs = []}     P? eq = []
-takeWhile⁻ {xs = x ∷ xs} P? eq with P? x
-... | yes px = px ∷ takeWhile⁻ P? (List.∷-injectiveʳ eq)
-... | no ¬px = case eq of λ ()
-
 all-takeWhile : (P? : Decidable P) → ∀ xs → All P (takeWhile P? xs)
 all-takeWhile P? []       = []
 all-takeWhile P? (x ∷ xs) with P? x
@@ -765,3 +759,12 @@ map-compose = map-∘
 "Warning: map-compose was deprecated in v2.1.
 Please use map-∘ instead."
 #-}
+
+-- Version 2.2
+
+takeWhile⁻ : (P? : Decidable P) → takeWhile P? xs ≡ xs → All P xs
+takeWhile⁻ {xs = xs} P? eq rewrite sym eq = all-takeWhile P? xs
+{-# WARNING_ON_USAGE takeWhile⁻
+"Warning: takeWhile⁻ was deprecated in v2.2.
+Please use all-takeWhile instead."
+#-}