From c667ad6a2a56bb2819b16559c976823d4da0e71f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 25 Feb 2026 15:05:11 +0000 Subject: [PATCH 1/2] [ refactor ] fix #2865 --- CHANGELOG.md | 11 +++++++ .../List/NonEmpty/Relation/Unary/Any.agda | 21 +++++++++++-- src/Data/List/Relation/Unary/Any.agda | 30 +++++++++++++++---- .../List/Relation/Unary/Any/Properties.agda | 2 +- 4 files changed, 54 insertions(+), 10 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f83411bc22..8323d68d6f 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/src/Data/List/NonEmpty/Relation/Unary/Any.agda b/src/Data/List/NonEmpty/Relation/Unary/Any.agda index 62a5906480..47817d5a72 100644 --- a/src/Data/List/NonEmpty/Relation/Unary/Any.agda +++ b/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." +#-} diff --git a/src/Data/List/Relation/Unary/Any.agda b/src/Data/List/Relation/Unary/Any.agda index f5500a5261..5c1eac3c63 100644 --- a/src/Data/List/Relation/Unary/Any.agda +++ b/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." +#-} diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda index f9b139dfdb..80e03f0b4b 100644 --- a/src/Data/List/Relation/Unary/Any/Properties.agda +++ b/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 From c33c667ac30f17a69d967e3196dc09ebb42e6c22 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 27 Feb 2026 10:10:16 +0000 Subject: [PATCH 2/2] refactor: another round of renaming --- CHANGELOG.md | 4 ++-- .../List/NonEmpty/Relation/Unary/Any.agda | 21 +++---------------- src/Data/List/Relation/Unary/Any.agda | 16 +++++--------- .../List/Relation/Unary/Any/Properties.agda | 2 +- 4 files changed, 11 insertions(+), 32 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8323d68d6f..095ccf0dac 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -91,8 +91,7 @@ Deprecated names * In `Data.List.Relation.Unary.Any`: ```agda - satisfied ↦ any⇒satisfiable - satisfiable ↦ satisfiable⁺ + satisfied ↦ satisfiable ``` * In `Data.Rational.Properties`: @@ -286,6 +285,7 @@ Additions to existing modules * In `Data.List.Relation.Unary.Any`: ```agda + satisfiable⁺ : Satisfiable P → Satisfiable (Any P) satisfiable⁻ : Satisfiable (Any P) → Satisfiable P ``` diff --git a/src/Data/List/NonEmpty/Relation/Unary/Any.agda b/src/Data/List/NonEmpty/Relation/Unary/Any.agda index 47817d5a72..59d5c690f5 100644 --- a/src/Data/List/NonEmpty/Relation/Unary/Any.agda +++ b/src/Data/List/NonEmpty/Relation/Unary/Any.agda @@ -42,21 +42,6 @@ map g (there pxs) = there (List.map g pxs) ------------------------------------------------------------------------ -- Predicates -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." -#-} +satisfiable : Any P xs → Satisfiable P +satisfiable (here px) = _ , px +satisfiable (there pxs) = List.satisfiable pxs diff --git a/src/Data/List/Relation/Unary/Any.agda b/src/Data/List/Relation/Unary/Any.agda index 5c1eac3c63..99d71b280d 100644 --- a/src/Data/List/Relation/Unary/Any.agda +++ b/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. -any⇒satisfiable : Any P xs → Satisfiable P -any⇒satisfiable (here px) = _ , px -any⇒satisfiable (there pxs) = any⇒satisfiable pxs +satisfiable : Any P xs → Satisfiable P +satisfiable (here px) = _ , px +satisfiable (there pxs) = satisfiable pxs toSum : Any P (x ∷ xs) → P x ⊎ Any P xs toSum (here px) = inj₁ px @@ -114,14 +114,8 @@ Please use any? instead." -- Version 2.4 -satisfied = any⇒satisfiable +satisfied = 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." +Please use satisfiable instead." #-} diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda index 80e03f0b4b..d60e0cfb31 100644 --- a/src/Data/List/Relation/Unary/Any/Properties.agda +++ b/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.any⇒satisfiable Rxys)))) , Any.map (proj₂ ∘ resp) Rxys + in here (proj₁ (resp (proj₂ (Any.satisfiable Rxys)))) , Any.map (proj₂ ∘ resp) Rxys ... | inj₂ Rc = let pxs , qys = cartesianProductWith⁻ resp xs ys Rc in there pxs , qys