deprecate: names for deMorgan lemmas (#2837)

Author: jamesmckinna

CHANGELOG.md

@@ -53,6 +53,12 @@ Deprecated names
   interchange  ↦   medial
   ```
 
+* In `Data.Fin.Properties`:
+  ```agda
+  ¬∀⟶∃¬-smallest  ↦   ¬∀⇒∃¬-smallest
+  ¬∀⟶∃¬-          ↦   ¬∀⇒∃¬
+  ```
+
 * In `Relation.Nullary.Negation`:
   ```agda
   ∃⟶¬∀¬  ↦   ∃⇒¬∀¬

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."
+#-}