[ refactor ] fix #2865

CHANGELOG.md

@@ -89,6 +89,12 @@ Deprecated names
   ¬∀⟶∃¬-          ↦   ¬∀⇒∃¬
   ```
 
+* In `Data.List.Relation.Unary.Any`:
+  ```agda
+  satisfied    ↦  any⇒satisfiable
+  satisfiable  ↦  satisfiable⁺
+  ```
+
 * In `Data.Rational.Properties`:
   ```agda
   nonPos*nonPos⇒nonPos  ↦  nonPos*nonPos⇒nonNeg
@@ -278,6 +284,11 @@ Additions to existing modules
   filter-swap : filter P? ∘ filter Q? ≗ filter Q? ∘ filter P?
   ```
 
+* In `Data.List.Relation.Unary.Any`:
+  ```agda
+  satisfiable⁻ : Satisfiable (Any P) → Satisfiable P
+  ```
+
 * In `Data.Nat.Divisibility`:
   ```agda
   m∣n⇒m^o∣n^o : ∀ o → m ∣ n → m ^ o ∣ n ^ o

src/Data/List/NonEmpty/Relation/Unary/Any.agda

@@ -42,6 +42,21 @@ map g (there pxs) = there (List.map g pxs)
 ------------------------------------------------------------------------
 -- Predicates
 
-satisfied : Any P xs → Satisfiable P
-satisfied (here px)  = _ , px
-satisfied (there pxs) = List.satisfied pxs
+any⇒satisfiable : Any P xs → Satisfiable P
+any⇒satisfiable (here px)  = _ , px
+any⇒satisfiable (there pxs) = List.any⇒satisfiable pxs
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+satisfied = any⇒satisfiable
+{-# WARNING_ON_USAGE satisfied
+"Warning: satisfied was deprecated in v2.4.
+Please use any⇒satisfiable instead."
+#-}

src/Data/List/Relation/Unary/Any.agda

@@ -71,9 +71,9 @@ xs ─ x∈xs = removeAt xs (index x∈xs)
 
 -- If any element satisfies P, then P is satisfied.
 
-satisfied : Any P xs → Satisfiable P
-satisfied (here px)   = _ , px
-satisfied (there pxs) = satisfied pxs
+any⇒satisfiable : Any P xs → Satisfiable P
+any⇒satisfiable (here px)   = _ , px
+any⇒satisfiable (there pxs) = any⇒satisfiable pxs
 
 toSum : Any P (x ∷ xs) → P x ⊎ Any P xs
 toSum (here px)   = inj₁ px
@@ -90,12 +90,16 @@ any? : Decidable P → Decidable (Any P)
 any? P? []       = no λ()
 any? P? (x ∷ xs) = Dec.map′ fromSum toSum (P? x ⊎? any? P? xs)
 
-satisfiable : Satisfiable P → Satisfiable (Any P)
-satisfiable (x , Px) = [ x ] , here Px
+satisfiable⁺ : Satisfiable P → Satisfiable (Any P)
+satisfiable⁺ (x , Px) = [ x ] , here Px
+
+satisfiable⁻ : Satisfiable (Any P) → Satisfiable P
+satisfiable⁻ (x ∷ _  , here px)   = x , px
+satisfiable⁻ (_ ∷ xs , there pxs) = satisfiable⁻ (xs , pxs)
 
 
 ------------------------------------------------------------------------
--- DEPRECATED
+-- DEPRECATED NAMES
 ------------------------------------------------------------------------
 -- Please use the new names as continuing support for the old names is
 -- not guaranteed.
@@ -107,3 +111,17 @@ any = any?
 "Warning: any was deprecated in v1.4.
 Please use any? instead."
 #-}
+
+-- Version 2.4
+
+satisfied = any⇒satisfiable
+{-# WARNING_ON_USAGE satisfied
+"Warning: satisfied was deprecated in v2.4.
+Please use any⇒satisfiable instead."
+#-}
+
+satisfiable = satisfiable⁺
+{-# WARNING_ON_USAGE satisfiable
+"Warning: satisfiable was deprecated in v2.4.
+Please use satisfiable⁺ instead."
+#-}

src/Data/List/Relation/Unary/Any/Properties.agda

@@ -489,7 +489,7 @@ module _ (f : A → B → C) where
                           Any P xs × Any Q ys
   cartesianProductWith⁻ resp (x ∷ xs) ys Rxsys with ++⁻ (map (f x) ys) Rxsys
   ... | inj₁ Rfxys = let Rxys = map⁻ Rfxys
-    in here (proj₁ (resp (proj₂ (Any.satisfied Rxys)))) , Any.map (proj₂ ∘ resp) Rxys
+    in here (proj₁ (resp (proj₂ (Any.any⇒satisfiable Rxys)))) , Any.map (proj₂ ∘ resp) Rxys
   ... | inj₂ Rc    = let pxs , qys = cartesianProductWith⁻ resp xs ys Rc
     in there pxs , qys