[fix] issue agda#1726

Author: jamesmckinna

CHANGELOG.md

@@ -866,6 +866,11 @@ Deprecated names
   raise    ↦  _↑ʳ_
   ```
 
+  Issue #1726: the relation `_≺_` and its single constructor `_≻toℕ_`
+  have been deprecated in favour of their extensional equivalent `_<_`
+  but omitting the inversion principle which pattern matching on `_≻toℕ_`
+  would achieve; this instead is proxied by the property `Data.Fin.Properties.toℕ<`.
+
 * In `Data.Fin.Properties`:
   ```
   toℕ-raise        ↦ toℕ-↑ʳ
@@ -876,6 +881,9 @@ Deprecated names
   eq?              ↦ inj⇒≟
   ```
 
+  Likewise under issue #1726: the properties `≺⇒<′` and `<′⇒≺` have been deprecated
+  in favour of their proxy counterparts `<⇒<′` and `<′⇒<`.
+
 * In `Data.Fin.Permutation.Components`:
   ```
   reverse            ↦ Data.Fin.Base.opposite

src/Data/Fin/Base.agda

@@ -332,32 +332,12 @@ NB argument order has been flipped:
 the left-hand argument is the Fin m
 the right-hand is the Nat index increment."
 #-}
-
 ------------------------------------------------------------------------
 -- _≺_
 
 data _≺_ : ℕ → ℕ → Set where
   _≻toℕ_ : ∀ n (i : Fin n) → toℕ i ≺ n
 
-------------------------------------------------------------------------
--- properties of _≺_
--- introduce new proofs, actually simplified compared to original
--- so that Data.Fin.Properties doesn't mention the constructor
-
-private
-
-  z≺s : ∀ {n} → zero ≺ suc n
-  z≺s = _ ≻toℕ zero
-
-  s≺s : ∀ {m n} → m ≺ n → suc m ≺ suc n
-  s≺s (n ≻toℕ i) = (suc n) ≻toℕ (suc i)
-
--- new lemma, nowhere else used except to define deprecated property later
-
-<⇒≺ : ℕ._<_ ⇒ _≺_
-<⇒≺ {zero}  z<s      = z≺s
-<⇒≺ {suc m} (s<s lt) = s≺s (<⇒≺ lt)
-
 -- now do the deprecation!
 {-# WARNING_ON_USAGE _≺_
 "Warning: _≺_ was deprecated in v2.0.

src/Data/Fin/Properties.agda

@@ -6,6 +6,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --warn=noUserWarning #-} -- for issue #1726
 
 module Data.Fin.Properties where
 
@@ -1123,8 +1124,21 @@ Please use inj⇒≟ instead."
 #-}
 ------------------------------------------------------------------------
 -- deprecated properties of deprecated _≺_
+-- introduce new proofs, actually simplified compared to original
+-- so that Data.Fin.Properties doesn't mention the constructor
 
 private
+
+  z≺s : ∀ {n} → zero ≺ suc n
+  z≺s = _ ≻toℕ zero
+
+  s≺s : ∀ {m n} → m ≺ n → suc m ≺ suc n
+  s≺s (n ≻toℕ i) = (suc n) ≻toℕ (suc i)
+
+  <⇒≺ : ℕ._<_ ⇒ _≺_
+  <⇒≺ {zero}  z<s      = z≺s
+  <⇒≺ {suc m} (s<s lt) = s≺s (<⇒≺ lt)
+
   ≺⇒< : _≺_ ⇒ ℕ._<_
   ≺⇒< (n ≻toℕ i) = toℕ<n i