Deprecate _∷ʳ'_ (both versions) and decidable' functions in favour of version ending in prime. (#1202)

Author: elsanussi-s-mneina

CHANGELOG.md

@@ -37,6 +37,13 @@ Deprecated names
 * The proofs `replace-equality` from `Algebra.Properties.(Lattice/DistributiveLattice/BooleanAlgebra)`
   have been deprecated in favour of the proofs in the new `Algebra.Construct.Subst.Equality` module.
 
+* In order to be consistent in usage of \prime character and apostrophe in identifiers, the following three names were deprecated in favor of their replacement that ends with a \prime character.
+
+  * `Data.List.Base.InitLast._∷ʳ'_` ↦ `Data.List.Base.InitLast._∷ʳ′_`
+  * `Data.List.NonEmpty.SnocView._∷ʳ'_` ↦ `Data.List.NonEmpty.SnocView._∷ʳ′_`
+  * `Relation.Binary.Construct.StrictToNonStrict.decidable'` ↦ `Relation.Binary.Construct.StrictToNonStrict.decidable′`
+
+
 Other major additions
 ---------------------
 

src/Data/List/Base.agda

@@ -364,17 +364,19 @@ xs ∷ʳ? x = maybe′ (xs ∷ʳ_) 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
 
 ------------------------------------------------------------------------
 -- Splitting a list
@@ -440,3 +442,13 @@ boolSpan p (x ∷ xs) with p x
 
 boolBreak : (A → Bool) → List A → (List A × List A)
 boolBreak p = boolSpan (not ∘ p)
+
+-- Version 1.4
+
+infixl 5 _∷ʳ'_
+_∷ʳ'_ : (xs : List A) (x : A) → InitLast (xs ∷ʳ x)
+_∷ʳ'_ = InitLast._∷ʳ′_
+{-# WARNING_ON_USAGE _∷ʳ'_
+"Warning: _∷ʳ'_ (ending in an apostrophe) was deprecated in v1.4.
+Please use _∷ʳ′_ (ending in a prime) instead."
+#-}

src/Data/List/NonEmpty.agda

@@ -193,7 +193,7 @@ data SnocView {A : Set a} : List⁺ A → Set a where
 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 ∷ .(xs List.∷ʳ y)) | xs List.∷ʳ′ y = (x ∷ xs) ∷ʳ′ y
 
 -- The last element in the list.
 
@@ -326,3 +326,20 @@ private
     wordsBy (ℕ._≡ᵇ 1) (1 ∷ 2 ∷ 3 ∷ 1 ∷ 1 ∷ 2 ∷ 1 ∷ []) ≡
     (2 ∷⁺ [ 3 ]) ∷ [ 2 ] ∷ []
   wordsBy-≡1 = refl
+
+  ------------------------------------------------------------------------
+  -- DEPRECATED
+  ------------------------------------------------------------------------
+  -- Please use the new names as continuing support for the old names is
+  -- not guaranteed.
+
+  -- Version 1.4
+
+  infixl 5 _∷ʳ'_
+
+  _∷ʳ'_ : (xs : List A) (x : A) → SnocView (xs ∷ʳ x)
+  _∷ʳ'_ = SnocView._∷ʳ′_
+  {-# WARNING_ON_USAGE _∷ʳ'_
+  "Warning: _∷ʳ'_ (ending in an apostrophe) was deprecated in v1.4.
+  Please use _∷ʳ′_ (ending in a prime) instead."
+  #-}

src/Relation/Binary/Construct/StrictToNonStrict.agda

@@ -96,8 +96,8 @@ total <-tri x y with <-tri x y
 decidable : Decidable _≈_ → Decidable _<_ → Decidable _≤_
 decidable ≈-dec <-dec x y = <-dec x y ⊎-dec ≈-dec x y
 
-decidable' : Trichotomous _≈_ _<_ → Decidable _≤_
-decidable' compare x y with compare x y
+decidable′ : Trichotomous _≈_ _<_ → Decidable _≤_
+decidable′ compare x y with compare x y
 ... | tri< x<y _   _ = yes (inj₁ x<y)
 ... | tri≈ _   x≈y _ = yes (inj₂ x≈y)
 ... | tri> x≮y x≉y _ = no [ x≮y , x≉y ]′
@@ -139,6 +139,22 @@ isDecTotalOrder : IsStrictTotalOrder _≈_ _<_ → IsDecTotalOrder _≈_ _≤_
 isDecTotalOrder STO = record
   { isTotalOrder = isTotalOrder STO
   ; _≟_          = S._≟_
-  ; _≤?_         = decidable' S.compare
+  ; _≤?_         = decidable′ S.compare
   }
   where module S = IsStrictTotalOrder STO
+
+
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 1.4
+
+decidable' : Trichotomous _≈_ _<_ → Decidable _≤_
+decidable' = decidable′
+{-# WARNING_ON_USAGE decidable'
+"Warning: decidable' (ending in an apostrophe) was deprecated in v1.4.
+Please use decidable′ (ending in a prime) instead."
+#-}