From ecd3b061fe00702c68d646f207c0619cd9c53559 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Sat, 28 Dec 2024 14:30:38 +0000
Subject: [PATCH] =?UTF-8?q?[=20refactor=20]=20Change=20definition=20of=20`?=
 =?UTF-8?q?Data.Nat.Base.=5F=E2=89=A4=E2=80=B2=5F`=20(#2523)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* refactor in line with #2504 / #2519

* tidy up `CHANGELOG` ahead of merge conflict resolution

* refactor: redefine pattern synonym
---
 CHANGELOG.md                 | 2 +-
 src/Data/Nat/Base.agda       | 6 ++++--
 src/Data/Nat/Properties.agda | 4 ++--
 3 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3c1c689d57..5c3dfd2747 100644
--- a/CHANGELOG.md
+++ b/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
 ------------------
diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 58e3e2644f..e62ec43436 100644
--- a/src/Data/Nat/Base.agda
+++ b/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
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 044e9bdefe..3537b3298a 100644
--- a/src/Data/Nat/Properties.agda
+++ b/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)
 
 ≤⇒≤′ : _≤_ ⇒ _≤′_