Rename all and any to all? and any? for consistency (#1260)

Author: umazalakain

CHANGELOG.md

@@ -90,6 +90,11 @@ Deprecated names
   *-+-isSemiringWithoutAnnihilatingZero  ↦  +-*-isSemiringWithoutAnnihilatingZero
   ```
 
+* `Data.List.Relation.Unary.Any.any` to `Data.List.Relation.Unary.Any.any?`
+* `Data.List.Relation.Unary.All.all` to `Data.List.Relation.Unary.All.all?`
+* `Data.Vec.Relation.Unary.Any.any` to `Data.Vec.Relation.Unary.Any.any?`
+* `Data.Vec.Relation.Unary.All.all` to `Data.Vec.Relation.Unary.All.all?`
+
 New modules
 -----------
 

src/Data/List/Countdown.agda

@@ -149,7 +149,7 @@ emptyFromList counted complete = empty record
 -- Finds out if an element has been counted yet.
 
 lookup : ∀ {counted n} → counted ⊕ n → ∀ x → Dec (x ∈ counted)
-lookup {counted} _ x = Any.any (_≟_ x) counted
+lookup {counted} _ x = Any.any? (_≟_ x) counted
 
 -- When no element remains to be counted all elements have been
 -- counted.

src/Data/List/Membership/DecSetoid.agda

@@ -10,7 +10,7 @@ open import Relation.Binary using (Decidable; DecSetoid)
 
 module Data.List.Membership.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where
 
-open import Data.List.Relation.Unary.Any using (any)
+open import Data.List.Relation.Unary.Any using (any?)
 open DecSetoid DS
 
 ------------------------------------------------------------------------
@@ -24,4 +24,4 @@ open import Data.List.Membership.Setoid (DecSetoid.setoid DS) public
 infix 4 _∈?_
 
 _∈?_ : Decidable _∈_
-x ∈? xs = any (x ≟_) xs
+x ∈? xs = any? (x ≟_) xs

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

@@ -212,9 +212,9 @@ module _ {P : Pred A p} where
 
 module _ {P : Pred A p} where
 
-  all : Decidable P → Decidable (All P)
-  all p []       = yes []
-  all p (x ∷ xs) = Dec.map′ (uncurry _∷_) uncons (p x ×-dec all p xs)
+  all? : Decidable P → Decidable (All P)
+  all? p []       = yes []
+  all? p (x ∷ xs) = Dec.map′ (uncurry _∷_) uncons (p x ×-dec all? p xs)
 
   universal : Universal P → Universal (All P)
   universal u []       = []
@@ -227,3 +227,9 @@ module _ {P : Pred A p} where
 
   satisfiable : Satisfiable (All P)
   satisfiable = [] , []
+
+all = all?
+{-# WARNING_ON_USAGE all
+"Warning: all was deprecated in v1.4.
+Please use all? instead."
+#-}

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

@@ -71,7 +71,7 @@ module _ {s} {S : Rel A s} where
 allPairs? : B.Decidable R → U.Decidable (AllPairs R)
 allPairs? R? []       = yes []
 allPairs? R? (x ∷ xs) =
-  Dec.map′ (uncurry _∷_) uncons (All.all (R? x) xs ×-dec allPairs? R? xs)
+  Dec.map′ (uncurry _∷_) uncons (All.all? (R? x) xs ×-dec allPairs? R? xs)
 
 irrelevant : B.Irrelevant R → U.Irrelevant (AllPairs R)
 irrelevant irr []           []           = refl

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

@@ -94,9 +94,15 @@ module _ {P : Pred A p} {x xs} where
 
 module _ {P : Pred A p} where
 
-  any : Decidable P → Decidable (Any P)
-  any P? []       = no λ()
-  any P? (x ∷ xs) = Dec.map′ fromSum toSum (P? x ⊎-dec any P? xs)
+  any? : Decidable P → Decidable (Any P)
+  any? P? []       = no λ()
+  any? P? (x ∷ xs) = Dec.map′ fromSum toSum (P? x ⊎-dec any? P? xs)
 
   satisfiable : Satisfiable P → Satisfiable (Any P)
   satisfiable (x , Px) = [ x ] , here Px
+
+any = any?
+{-# WARNING_ON_USAGE any
+"Warning: any was deprecated in v1.4.
+Please use any? instead."
+#-}

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

@@ -9,7 +9,7 @@
 module Data.List.Relation.Unary.Grouped where
 
 open import Data.List using (List; []; _∷_; map)
-open import Data.List.Relation.Unary.All as All using (All; []; _∷_; all)
+open import Data.List.Relation.Unary.All as All using (All; []; _∷_; all?)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Data.Product using (_×_; _,_)
 open import Relation.Binary as B using (REL; Rel)
@@ -32,7 +32,7 @@ module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} where
   grouped? : B.Decidable _≈_ → U.Decidable (Grouped _≈_)
   grouped? _≟_ [] = yes []
   grouped? _≟_ (x ∷ []) = yes ([] ∷≉ [])
-  grouped? _≟_ (x ∷ y ∷ xs) = map′ from to ((x ≟ y ⊎-dec all (λ z → ¬? (x ≟ z)) (y ∷ xs)) ×-dec (grouped? _≟_ (y ∷ xs))) where
+  grouped? _≟_ (x ∷ y ∷ xs) = map′ from to ((x ≟ y ⊎-dec all? (λ z → ¬? (x ≟ z)) (y ∷ xs)) ×-dec (grouped? _≟_ (y ∷ xs))) where
     from : ((x ≈ y) ⊎ All (λ z → ¬ (x ≈ z)) (y ∷ xs)) × Grouped _≈_ (y ∷ xs) → Grouped _≈_ (x ∷ y ∷ xs)
     from (inj₁ x≈y          , grouped[y∷xs]) = x≈y          ∷≈ grouped[y∷xs]
     from (inj₂ all[x≉,y∷xs] , grouped[y∷xs]) = all[x≉,y∷xs] ∷≉ grouped[y∷xs]

src/Data/Vec/Membership/DecSetoid.agda

@@ -11,7 +11,7 @@ open import Relation.Binary using (DecSetoid)
 module Data.Vec.Membership.DecSetoid {c ℓ} (DS : DecSetoid c ℓ) where
 
 open import Data.Vec.Base using (Vec)
-open import Data.Vec.Relation.Unary.Any using (any)
+open import Data.Vec.Relation.Unary.Any using (any?)
 open import Relation.Nullary using (Dec)
 open DecSetoid DS renaming (Carrier to A)
 
@@ -26,4 +26,4 @@ open import Data.Vec.Membership.Setoid setoid public
 infix 4 _∈?_
 
 _∈?_ : ∀ x {n} (xs : Vec A n) → Dec (x ∈ xs)
-x ∈? xs = any (x ≟_) xs
+x ∈? xs = any? (x ≟_) xs

src/Data/Vec/Relation/Unary/All.agda

@@ -88,9 +88,9 @@ module _ {P : Pred A p} {Q : Pred B q} {R : Pred C r} where
 
 module _ {P : Pred A p} where
 
-  all : ∀ {n} → Decidable P → Decidable (All P {n})
-  all P? []       = yes []
-  all P? (x ∷ xs) = Dec.map′ (uncurry _∷_) uncons (P? x ×-dec all P? xs)
+  all? : ∀ {n} → Decidable P → Decidable (All P {n})
+  all? P? []       = yes []
+  all? P? (x ∷ xs) = Dec.map′ (uncurry _∷_) uncons (P? x ×-dec all? P? xs)
 
   universal : Universal P → ∀ {n} → Universal (All P {n})
   universal u []       = []
@@ -104,3 +104,9 @@ module _ {P : Pred A p} where
   satisfiable : Satisfiable P → ∀ {n} → Satisfiable (All P {n})
   satisfiable (x , p) {zero}  = [] , []
   satisfiable (x , p) {suc n} = Prod.map (x ∷_) (p ∷_) (satisfiable (x , p))
+
+all = all?
+{-# WARNING_ON_USAGE all
+"Warning: all was deprecated in v1.4.
+Please use all? instead."
+#-}

src/Data/Vec/Relation/Unary/AllPairs.agda

@@ -71,7 +71,7 @@ module _ {s} {S : Rel A s} where
 allPairs? : ∀ {n} → B.Decidable R → U.Decidable (AllPairs R {n})
 allPairs? R? []       = yes []
 allPairs? R? (x ∷ xs) =
-  Dec.map′ (uncurry _∷_) uncons (All.all (R? x) xs ×-dec allPairs? R? xs)
+  Dec.map′ (uncurry _∷_) uncons (All.all? (R? x) xs ×-dec allPairs? R? xs)
 
 irrelevant : ∀ {n} → B.Irrelevant R → U.Irrelevant (AllPairs R {n})
 irrelevant irr []           []           = refl