From b3265a62014ad8cfd08f660cefb9f02e91e3e503 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 9 Oct 2025 10:52:00 +0100
Subject: [PATCH] deprecate: names for deMorgan lemmas

---
 CHANGELOG.md                 |  6 ++++++
 src/Data/Fin/Properties.agda | 25 +++++++++++++++++++------
 2 files changed, 25 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7b117e30da..4ad53a884b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -46,6 +46,12 @@ Deprecated names
   interchange  ↦   medial
   ```
 
+* In `Data.Fin.Properties`:
+  ```agda
+  ¬∀⟶∃¬-smallest  ↦   ¬∀⇒∃¬-smallest
+  ¬∀⟶∃¬-          ↦   ¬∀⇒∃¬
+  ```
+
 New modules
 -----------
 
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 2b3e2f1285..84638a3707 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -1052,20 +1052,20 @@ private
 -- If a decidable predicate P over a finite set is sometimes false,
 -- then we can find the smallest value for which this is the case.
 
-¬∀⟶∃¬-smallest : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
+¬∀⇒∃¬-smallest : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
                  ¬ (∀ i → P i) → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
-¬∀⟶∃¬-smallest zero    P P? ¬∀P = contradiction (λ()) ¬∀P
-¬∀⟶∃¬-smallest (suc n) P P? ¬∀P with P? zero
+¬∀⇒∃¬-smallest zero    P P? ¬∀P = contradiction (λ()) ¬∀P
+¬∀⇒∃¬-smallest (suc n) P P? ¬∀P with P? zero
 ... | false because [¬P₀] = (zero , invert [¬P₀] , λ ())
 ... | true  because  [P₀] = map suc (map id (∀-cons (invert [P₀])))
-  (¬∀⟶∃¬-smallest n (P ∘ suc) (P? ∘ suc) (¬∀P ∘ (∀-cons (invert [P₀]))))
+  (¬∀⇒∃¬-smallest n (P ∘ suc) (P? ∘ suc) (¬∀P ∘ (∀-cons (invert [P₀]))))
 
 -- When P is a decidable predicate over a finite set the following
 -- lemma can be proved.
 
-¬∀⟶∃¬ : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
+¬∀⇒∃¬ : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
           ¬ (∀ i → P i) → (∃ λ i → ¬ P i)
-¬∀⟶∃¬ n P P? ¬P = map id proj₁ (¬∀⟶∃¬-smallest n P P? ¬P)
+¬∀⇒∃¬ n P P? ¬P = map id proj₁ (¬∀⇒∃¬-smallest n P P? ¬P)
 
 ------------------------------------------------------------------------
 -- Properties of functions to and from Fin
@@ -1277,3 +1277,16 @@ Please use <⇒<′ instead."
 "Warning: <′⇒≺ was deprecated in v2.0.
 Please use <′⇒< instead."
 #-}
+
+-- Version 2.4
+
+¬∀⟶∃¬-smallest = ¬∀⇒∃¬-smallest
+{-# WARNING_ON_USAGE ¬∀⟶∃¬-smallest
+"Warning: ¬∀⟶∃¬-smallest was deprecated in v2.4.
+Please use ¬∀⇒∃¬-smallest instead."
+#-}
+¬∀⟶∃¬ = ¬∀⇒∃¬
+{-# WARNING_ON_USAGE ¬∀⟶∃¬
+"Warning: ¬∀⟶∃¬ was deprecated in v2.4.
+Please use ¬∀⇒∃¬ instead."
+#-}