[ refactor ] rename constructors of Data.List.Base.InitLast and friends

CHANGELOG.md

@@ -152,6 +152,12 @@ Non-backwards compatible changes
   counterparts. Consider using `viaList` if you want a lawful lifting
   of `take` or `drop`.
 
+* [Issue #3089](https://github.com/agda/agda-stdlib/issues/3089)
+  The constructor names for the `Data.List.Base.InitLast` view of `List`,
+  and their associated definitions, have been renamed with a *prefix*
+  backtick, in line with existing conventions about 'quoted' syntax for
+  defined function symbols.
+
 * [Issue #2319](https://github.com/agda/agda-stdlib/issues/2319)
   The custom syntax for `swap` and `prep` steps in `PermutationReasoning`,
   defined in `Data.List.Relation.Binary.Permutation.{Propositional|Setoid}`,
@@ -216,6 +222,16 @@ Deprecated names
   gcd[0,0]≡0 ↦ gcd[i,i]≡∣i∣
   ```
 
+* In `Data.List.Base`:
+  ```agda
+  pattern _∷ʳ′_ ↦ _‵∷ʳ_
+  ```
+
+* In `Data.List.NonEmpty.Base`:
+  ```agda
+  pattern _∷ʳ′_ ↦ _‵∷ʳ_
+  ```
+
 * In `Data.Nat.GCD`:
   ```agda
   gcd[0,0]≡0 ↦ gcd[n,n]≡n

src/Data/List/Base.agda

@@ -255,23 +255,23 @@ xs ∷ʳ x = xs ++ [ x ]
 
 -- Backwards initialisation
 
-infixl 5 _∷ʳ′_
+infixl 5 _‵∷ʳ_
 
 data InitLast {A : Set a} : List A → Set a where
   []    : InitLast []
-  _∷ʳ′_ : (xs : List A) (x : A) → InitLast (xs ∷ʳ x)
+  _‵∷ʳ_ : (xs : List A) (x : A) → InitLast (xs ∷ʳ x)
 
 initLast : (xs : List A) → InitLast xs
 initLast []               = []
 initLast (x ∷ xs)         with initLast xs
-... | []       = [] ∷ʳ′ x
-... | ys ∷ʳ′ y = (x ∷ ys) ∷ʳ′ y
+... | []       = [] ‵∷ʳ x
+... | ys ‵∷ʳ y = (x ∷ ys) ‵∷ʳ y
 
 -- uncons, but from the right
 unsnoc : List A → Maybe (List A × A)
 unsnoc as with initLast as
 ... | []       = nothing
-... | xs ∷ʳ′ x = just (xs , x)
+... | xs ‵∷ʳ x = just (xs , x)
 
 ------------------------------------------------------------------------
 -- Operations for deconstructing lists
@@ -598,3 +598,13 @@ product = foldr ℕ._*_ 1
 "Warning: product was deprecated in v2.3.
 Please use Data.Nat.ListAction.product instead."
 #-}
+
+-- Version 3.0
+
+infixl 5 _∷ʳ′_
+pattern _∷ʳ′_ = _‵∷ʳ_
+{-# WARNING_ON_USAGE _∷ʳ′_
+"Warning: _∷ʳ′_ was deprecated in v3.0.
+Please use _‵∷ʳ_ instead."
+#-}
+

src/Data/List/NonEmpty/Base.agda

@@ -201,21 +201,21 @@ xs ⁺∷ʳ x = toList xs ∷ʳ x
 
 -- A snoc-view of non-empty lists.
 
-infixl 5 _∷ʳ′_
+infixl 5 _‵∷ʳ_
 
 data SnocView {A : Set a} : List⁺ A → Set a where
-  _∷ʳ′_ : (xs : List A) (x : A) → SnocView (xs ∷ʳ x)
+  _‵∷ʳ_ : (xs : List A) (x : A) → SnocView (xs ∷ʳ x)
 
 snocView : (xs : List⁺ A) → SnocView xs
 snocView (x ∷ xs)              with List.initLast xs
-snocView (x ∷ .[])             | []            = []       ∷ʳ′ x
-snocView (x ∷ .(xs List.∷ʳ y)) | xs List.∷ʳ′ y = (x ∷ xs) ∷ʳ′ y
+snocView (x ∷ .[])             | []            = []       ‵∷ʳ x
+snocView (x ∷ .(xs List.∷ʳ y)) | xs List.‵∷ʳ y = (x ∷ xs) ‵∷ʳ y
 
 -- The last element in the list.
 
 private
   last′ : ∀ {l} → SnocView {A = A} l → A
-  last′ (_ ∷ʳ′ y) = y
+  last′ (_ ‵∷ʳ y) = y
 
 last : List⁺ A → A
 last = last′ ∘ snocView
@@ -336,3 +336,19 @@ private
                [ 2 ] ∷
                []
   wordsBy-≡1 = refl
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 3.0
+
+infixl 5 _∷ʳ′_
+pattern _∷ʳ′_ = _‵∷ʳ_
+{-# WARNING_ON_USAGE _∷ʳ′_
+"Warning: _∷ʳ′_ was deprecated in v3.0.
+Please use _‵∷ʳ_ instead."
+#-}

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

@@ -400,12 +400,12 @@ concat⁻ {xss = xs ∷ xss} pxs = ++⁻ˡ xs pxs ∷ concat⁻ (++⁻ʳ xs pxs)
 unsnoc⁺ : All P xs → Maybe.All (All P ⟨×⟩ P) (unsnoc xs)
 unsnoc⁺ {xs = xs} pxs with initLast xs
 unsnoc⁺ {xs = .[]}        pxs | []       = nothing
-unsnoc⁺ {xs = .(xs ∷ʳ x)} pxs | xs ∷ʳ′ x = just (∷ʳ⁻ pxs)
+unsnoc⁺ {xs = .(xs ∷ʳ x)} pxs | xs ‵∷ʳ x = just (∷ʳ⁻ pxs)
 
 unsnoc⁻ : Maybe.All (All P ⟨×⟩ P) (unsnoc xs) → All P xs
 unsnoc⁻ {xs = xs} pxs with initLast xs
 unsnoc⁻ {xs = .[]}        nothing           | []       = []
-unsnoc⁻ {xs = .(xs ∷ʳ x)} (just (pxs , px)) | xs ∷ʳ′ x = ∷ʳ⁺ pxs px
+unsnoc⁻ {xs = .(xs ∷ʳ x)} (just (pxs , px)) | xs ‵∷ʳ x = ∷ʳ⁺ pxs px
 
 ------------------------------------------------------------------------
 -- cartesianProductWith and cartesianProduct