refactor: more knock-ons

jamesmckinna · jamesmckinna · commit da62f21b658e · 2025-10-26T11:23:44.000Z
diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda
@@ -46,7 +46,7 @@ open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; cong; cong₂; subst; _≢_; sym)
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning; isEquivalence)
-open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎-dec_)
+open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎?_)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Unary using (Pred; Decidable; Satisfiable)
 
@@ -879,7 +879,7 @@ module _ {P : Pred (Subset (suc n)) ℓ} where
 anySubset? : ∀ {P : Pred (Subset n) ℓ} → Decidable P → Dec ∃⟨ P ⟩
 anySubset? {n = zero}  P? = Dec.map ∃-Subset-[]-⇔ (P? [])
 anySubset? {n = suc n} P? = Dec.map ∃-Subset-∷-⇔
-  (anySubset? (P? ∘ (inside ∷_)) ⊎-dec anySubset? (P? ∘ (outside ∷_)))
+  (anySubset? (P? ∘ (inside ∷_)) ⊎? anySubset? (P? ∘ (outside ∷_)))
 
 
 
diff --git a/src/Data/List/Fresh/Relation/Unary/All.agda b/src/Data/List/Fresh/Relation/Unary/All.agda
@@ -14,7 +14,7 @@ open import Data.Product.Base using (_×_; _,_; proj₁; uncurry)
 open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]′)
 open import Function.Base using (_∘_; _$_)
 open import Level using (Level; _⊔_; Lift)
-open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_)
+open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×?_)
 open import Relation.Unary as U
   using (Pred; IUniversal; Universal; Decidable; _⇒_; _∪_; _∩_)
 open import Relation.Binary.Core using (Rel)
@@ -67,7 +67,7 @@ module _ {R : Rel A r} {P : Pred A p} (P? : Decidable P) where
 
   all? : (xs : List# A R) → Dec (All P xs)
   all? []        = yes []
-  all? (x ∷# xs) = Dec.map′ (uncurry _∷_) uncons (P? x ×-dec all? xs)
+  all? (x ∷# xs) = Dec.map′ (uncurry _∷_) uncons (P? x ×? all? xs)
 
 ------------------------------------------------------------------------
 -- Generalised decidability procedure
diff --git a/src/Data/List/Fresh/Relation/Unary/Any.agda b/src/Data/List/Fresh/Relation/Unary/Any.agda
@@ -15,7 +15,7 @@ open import Data.Sum.Base using (_⊎_; [_,_]′; inj₁; inj₂)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (Level; _⊔_; Lift)
 open import Relation.Nullary.Negation using (¬_; contradiction)
-open import Relation.Nullary.Decidable as Dec using (Dec; no; _⊎-dec_)
+open import Relation.Nullary.Decidable as Dec using (Dec; no; _⊎?_)
 open import Relation.Unary  as U using (Pred; IUniversal; Universal; Decidable; _⇒_; _∪_; _∩_)
 open import Relation.Binary.Core using (Rel)
 
@@ -78,4 +78,4 @@ module _ {R : Rel A r} {P : Pred A p} (P? : Decidable P) where
 
   any? : (xs : List# A R) → Dec (Any P xs)
   any? []        = no (λ ())
-  any? (x ∷# xs) = Dec.map ⊎⇔Any (P? x ⊎-dec any? xs)
+  any? (x ∷# xs) = Dec.map ⊎⇔Any (P? x ⊎? any? xs)
diff --git a/src/Data/List/Relation/Unary/Grouped.agda b/src/Data/List/Relation/Unary/Grouped.agda
@@ -16,7 +16,7 @@ open import Relation.Binary.Core using (REL; Rel)
 open import Relation.Binary.Definitions as B
 open import Relation.Unary as U using (Pred)
 open import Relation.Nullary.Negation using (¬_)
-open import Relation.Nullary.Decidable as Dec using (yes; ¬?; _⊎-dec_; _×-dec_)
+open import Relation.Nullary.Decidable as Dec using (yes; ¬?; _⊎?_; _×?_)
 open import Level using (Level; _⊔_)
 
 private
@@ -45,7 +45,7 @@ module _ {_≈_ : Rel A ℓ} where
   grouped? _≟_ [] = yes []
   grouped? _≟_ (x ∷ []) = yes ([] ∷≉ [])
   grouped? _≟_ (x ∷ y ∷ xs) =
-    Dec.map′ from to ((x ≟ y ⊎-dec all? (λ z → ¬? (x ≟ z)) (y ∷ xs)) ×-dec (grouped? _≟_ (y ∷ xs)))
+    Dec.map′ from to ((x ≟ y ⊎? all? (λ z → ¬? (x ≟ z)) (y ∷ xs)) ×? (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]
diff --git a/src/Data/These/Properties.agda b/src/Data/These/Properties.agda
@@ -14,7 +14,7 @@ open import Function.Base using (_∘_)
 open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; cong; cong₂)
-open import Relation.Nullary.Decidable using (yes; no; map′; _×-dec_)
+open import Relation.Nullary.Decidable using (yes; no; map′; _×?_)
 
 ------------------------------------------------------------------------
 -- Equality
@@ -48,4 +48,4 @@ module _ {a b} {A : Set a} {B : Set b} where
   ≡-dec dec₁ dec₂ (these x a) (this y)    = no λ()
   ≡-dec dec₁ dec₂ (these x a) (that y)    = no λ()
   ≡-dec dec₁ dec₂ (these x a) (these y b) =
-    map′ (uncurry (cong₂ these)) these-injective (dec₁ x y ×-dec dec₂ a b)
+    map′ (uncurry (cong₂ these)) these-injective (dec₁ x y ×? dec₂ a b)
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda
@@ -20,7 +20,7 @@ open import Function.Base using (flip; _∘_; const)
 open import Function.Nary.NonDependent using (congₙ)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
-open import Relation.Nullary.Decidable.Core using (Dec; yes; map′; _×-dec_)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; map′; _×?_)
 open import Relation.Unary using (Pred; Decidable; Universal; Irrelevant; _⊆_; _∪_)
 
 open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
@@ -80,7 +80,7 @@ unnode (node p l r) = p , l , r
 all? : Decidable P → ∀ (t : Tree V l u n) → Dec (All P t)
 all? p? (leaf l<u)        = yes leaf
 all? p? (node kv l r bal) = map′ (uncurryₙ 3 node) unnode
-                                 (p? kv ×-dec all? p? l ×-dec all? p? r)
+                                 (p? kv ×? all? p? l ×? all? p? r)
 
 universal : Universal P → (t : Tree V l u n) → All P t
 universal u (leaf l<u)        = leaf
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
@@ -17,7 +17,7 @@ open import Data.Product.Base using (_,_; ∃; -,_; proj₁; proj₂)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (_∘′_; _∘_)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary.Decidable.Core using (Dec; no; map′; _⊎-dec_)
+open import Relation.Nullary.Decidable.Core using (Dec; no; map′; _⊎?_)
 open import Relation.Unary
 
 open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
@@ -107,7 +107,7 @@ module _ {hˡ hʳ h} {kv : K& V}
 any? : Decidable P → (t : Tree V l u n) → Dec (Any P t)
 any? P? (leaf _)          = no λ ()
 any? P? (node kv l r bal) = map′ fromSum toSum
-  (P? kv ⊎-dec any? P? l ⊎-dec any? P? r)
+  (P? kv ⊎? any? P? l ⊎? any? P? r)
 
 satisfiable : ∀ {k l u} → l <⁺ [ k ] → [ k ] <⁺ u →
               Satisfiable (P ∘ (k ,_)) →
diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda
@@ -28,7 +28,7 @@ open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
 open import Relation.Nullary.Decidable
-  using (Dec; does; yes; no; map′; _×-dec_)
+  using (Dec; does; yes; no; map′; _×?_)
 open import Relation.Nullary.Negation using (contradiction)
 
 import Data.Fin.Properties as Finₚ
@@ -54,7 +54,7 @@ module _ {xs ys : Vector A (suc n)} where
 ≗-dec {n = zero}  _≟_ xs ys = yes λ ()
 ≗-dec {n = suc n} _≟_ xs ys =
   map′ (Product.uncurry ∷-cong) ∷-injective
-       (head xs ≟ head ys ×-dec ≗-dec _≟_ (tail xs) (tail ys))
+       (head xs ≟ head ys ×? ≗-dec _≟_ (tail xs) (tail ys))
 
 ------------------------------------------------------------------------
 -- updateAt
diff --git a/src/Data/Vec/Relation/Binary/Lex/Core.agda b/src/Data/Vec/Relation/Binary/Lex/Core.agda
@@ -25,7 +25,7 @@ open import Relation.Binary.Structures using (IsPartialEquivalence)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; refl; cong)
 import Relation.Nullary as Nullary
-open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_; _⊎-dec_)
+open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×?_; _⊎?_)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 
 private
@@ -138,7 +138,7 @@ module _ {P : Set} {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
     decidable : ∀ {m n} → Decidable (_<ₗₑₓ_ {m} {n})
     decidable {m} {n} xs ys with m ℕ.≟ n
     decidable {_} {_} []       []       | yes refl = Dec.map P⇔[]<[] P?
-    decidable {_} {_} (x ∷ xs) (y ∷ ys) | yes refl = Dec.map ∷<∷-⇔ ((x ≺? y) ⊎-dec (x ≈? y) ×-dec (decidable xs ys))
+    decidable {_} {_} (x ∷ xs) (y ∷ ys) | yes refl = Dec.map ∷<∷-⇔ ((x ≺? y) ⊎? (x ≈? y) ×? (decidable xs ys))
     decidable {_} {_} _        _        | no  m≢n    = no (λ xs<ys → contradiction (length-equal xs<ys) m≢n)
 
   module _ (P-irrel  : Nullary.Irrelevant P)
diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
@@ -25,7 +25,7 @@ open import Relation.Binary.Structures
 open import Relation.Binary.Definitions
   using (Trans; Decidable; Reflexive; Sym)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-open import Relation.Nullary.Decidable using (yes; no; _×-dec_; map′)
+open import Relation.Nullary.Decidable using (yes; no; _×?_; map′)
 open import Relation.Unary using (Pred)
 
 private
@@ -111,7 +111,7 @@ decidable dec []       []       = yes []
 decidable dec []       (y ∷ ys) = no λ()
 decidable dec (x ∷ xs) []       = no λ()
 decidable dec (x ∷ xs) (y ∷ ys) =
-  map′ (uncurry _∷_) uncons (dec x y ×-dec decidable dec xs ys)
+  map′ (uncurry _∷_) uncons (dec x y ×? decidable dec xs ys)
 
 ------------------------------------------------------------------------
 -- Structures
diff --git a/src/Data/Vec/Relation/Unary/AllPairs.agda b/src/Data/Vec/Relation/Unary/AllPairs.agda
@@ -21,7 +21,7 @@ open import Relation.Binary.Definitions as B
 open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
 open import Relation.Binary.PropositionalEquality.Core using (refl; cong₂)
 open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
-open import Relation.Nullary.Decidable as Dec using (yes; no; _×-dec_)
+open import Relation.Nullary.Decidable as Dec using (yes; no; _×?_)
 
 ------------------------------------------------------------------------
 -- Definition
@@ -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 ×? allPairs? R? xs)
 
 irrelevant : ∀ {n} → B.Irrelevant R → U.Irrelevant (AllPairs R {n})
 irrelevant irr []           []           = refl
diff --git a/src/Data/Vec/Relation/Unary/Linked.agda b/src/Data/Vec/Relation/Unary/Linked.agda
@@ -19,7 +19,7 @@ import Relation.Binary.Definitions as B
 open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
 open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
-open import Relation.Nullary.Decidable as Dec using (yes; no; _×-dec_; map′)
+open import Relation.Nullary.Decidable as Dec using (yes; no; _×?_; map′)
 
 private
   variable
@@ -81,7 +81,7 @@ linked? : B.Decidable R → U.Decidable (Linked R {n})
 linked? R? []           = yes []
 linked? R? (x ∷ [])     = yes [-]
 linked? R? (x ∷ y ∷ xs) =
-  map′ (uncurry _∷_) < head , tail > (R? x y ×-dec linked? R? (y ∷ xs))
+  map′ (uncurry _∷_) < head , tail > (R? x y ×? linked? R? (y ∷ xs))
 
 irrelevant : B.Irrelevant R → U.Irrelevant (Linked R {n})
 irrelevant irr []           []           = refl
diff --git a/src/Relation/Binary/Construct/StrictToNonStrict.agda b/src/Relation/Binary/Construct/StrictToNonStrict.agda
@@ -28,7 +28,7 @@ open import Relation.Binary.Structures
 open import Relation.Binary.Definitions
   using (Transitive; Symmetric; Irreflexive; Antisymmetric; Trichotomous; Decidable
         ; Trans; Total; _Respects₂_; _Respectsʳ_; _Respectsˡ_; tri<; tri≈; tri>)
-open import Relation.Nullary.Decidable.Core using (_⊎-dec_; yes; no)
+open import Relation.Nullary.Decidable.Core using (_⊎?_; yes; no)
 open import Relation.Nullary.Negation.Core using (contradiction)
 
 ------------------------------------------------------------------------
@@ -101,7 +101,7 @@ total <-tri x y with <-tri x y
 ... | tri> x≮y x≉y x>y = inj₂ (inj₁ x>y)
 
 decidable : Decidable _≈_ → Decidable _<_ → Decidable _≤_
-decidable ≈-dec <-dec x y = <-dec x y ⊎-dec ≈-dec x y
+decidable ≈-dec <-dec x y = <-dec x y ⊎? ≈-dec x y
 
 decidable′ : Trichotomous _≈_ _<_ → Decidable _≤_
 decidable′ compare x y with compare x y
diff --git a/src/Relation/Binary/Construct/Union.agda b/src/Relation/Binary/Construct/Union.agda
@@ -15,7 +15,7 @@ open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (REL; Rel; _⇒_)
 open import Relation.Binary.Definitions
   using (Reflexive; Total; Minimum; Maximum; Symmetric; Irreflexive; Decidable; _Respects_; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
-open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_)
+open import Relation.Nullary.Decidable using (yes; no; _⊎?_)
 
 private
   variable
@@ -85,4 +85,4 @@ module _ (≈ : REL A B ℓ₁) (L : REL A B ℓ₂) (R : REL A B ℓ₃) where
 module _ {L : REL A B ℓ₁} {R : REL A B ℓ₂} where
 
   decidable : Decidable L → Decidable R → Decidable (L ∪ R)
-  decidable L? R? x y = L? x y ⊎-dec R? x y
+  decidable L? R? x y = L? x y ⊎? R? x y
