[ refactor ] Change definition of Data.Nat.Base._≤′_ (#2523)

* refactor in line with #2504 / #2519

* tidy up `CHANGELOG` ahead of merge conflict resolution

* refactor: redefine pattern synonym

Author: jamesmckinna

CHANGELOG.md

@@ -30,7 +30,7 @@ Non-backwards compatible changes
     them to name the operation `+`.
   * `distribˡ` and `distribʳ` are defined in the record.
 
-* [issue #2504](https://github.com/agda/agda-stdlib/issues/2504) In `Data.Nat.Base` the definition of `_≤‴_` has been modified to make the witness to equality explicit in a new `≤‴-reflexive` constructor; a pattern synonym ≤‴-refl` has been added for backwards compatibility but NB. the change in parametrisation means that this pattern is *not* well-formed if the old implicit arguments `m`,`n` are supplied explicitly.
+* [issue #2504](https://github.com/agda/agda-stdlib/issues/2504) and [issue #2519](https://github.com/agda/agda-stdlib/issues/2510) In `Data.Nat.Base` the definitions of `_≤′_` and `_≤‴_` have been modified to make the witness to equality explicit in new constructors `≤′-reflexive` and `≤‴-reflexive`; pattern synonyms `≤′-refl` and `≤‴-refl` have been added for backwards compatibility but NB. the change in parametrisation means that these patterns are *not* necessarily well-formed if the old implicit arguments `m`,`n` are supplied explicitly.
 
 Minor improvements
 ------------------

src/Data/Nat/Base.agda

@@ -338,8 +338,10 @@ suc n ! = suc n * n !
 infix 4 _≤′_ _<′_ _≥′_ _>′_
 
 data _≤′_ (m : ℕ) : ℕ → Set where
-  ≤′-refl :                         m ≤′ m
-  ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n
+  ≤′-reflexive : ∀ {n} → m ≡ n → m ≤′ n
+  ≤′-step : ∀ {n} → m ≤′ n → m ≤′ suc n
+
+pattern ≤′-refl {m} = ≤′-reflexive {n = m} refl
 
 _<′_ : Rel ℕ 0ℓ
 m <′ n = suc m ≤′ n

src/Data/Nat/Properties.agda

@@ -2039,11 +2039,11 @@ z≤′n {zero}  = ≤′-refl
 z≤′n {suc n} = ≤′-step z≤′n
 
 s≤′s : m ≤′ n → suc m ≤′ suc n
-s≤′s ≤′-refl        = ≤′-refl
+s≤′s (≤′-reflexive m≡n) = ≤′-reflexive (cong suc m≡n)
 s≤′s (≤′-step m≤′n) = ≤′-step (s≤′s m≤′n)
 
 ≤′⇒≤ : _≤′_ ⇒ _≤_
-≤′⇒≤ ≤′-refl        = ≤-refl
+≤′⇒≤ (≤′-reflexive m≡n) = ≤-reflexive m≡n
 ≤′⇒≤ (≤′-step m≤′n) = m≤n⇒m≤1+n (≤′⇒≤ m≤′n)
 
 ≤⇒≤′ : _≤_ ⇒ _≤′_