[ fix ] Relation.Nullary.Decidable.Core names for combinators

CHANGELOG.md

@@ -59,6 +59,14 @@ Deprecated names
   ¬∀⟶∃¬-          ↦   ¬∀⇒∃¬
   ```
 
+* In `Relation.Nullary.Decidable.Core`:
+  ```agda
+  ⊤-dec     ↦   ⊤?
+  ⊥-dec     ↦   ⊥?
+  _×-dec_  ↦   _×?_
+  _⊎-dec_  ↦   _⊎?_
+  _→-dec_  ↦   _→?_
+
 * In `Relation.Nullary.Negation`:
   ```agda
   ∃⟶¬∀¬  ↦   ∃⇒¬∀¬

doc/README/Design/Decidability.agda

@@ -106,8 +106,8 @@ suc m ≟₂ suc n = map′ (cong suc) suc-injective (m ≟₂ n)
 _ : (m n : ℕ) → does (5 + m ≟₂ 3 + n) ≡ does (2 + m ≟₂ n)
 _ = λ m n → refl
 
--- `map′` can be used in conjunction with combinators such as `_⊎-dec_` and
--- `_×-dec_` to build complex (simply typed) decision procedures.
+-- `map′` can be used in conjunction with combinators such as `_⊎?_` and
+-- `_×?_` to build complex (simply typed) decision procedures.
 
 module ListDecEq₀ {a} {A : Set a} (_≟ᴬ_ : (x y : A) → Dec (x ≡ y)) where
 
@@ -116,13 +116,13 @@ module ListDecEq₀ {a} {A : Set a} (_≟ᴬ_ : (x y : A) → Dec (x ≡ y)) whe
   []       ≟ᴸᴬ (y ∷ ys) = no λ ()
   (x ∷ xs) ≟ᴸᴬ []       = no λ ()
   (x ∷ xs) ≟ᴸᴬ (y ∷ ys) =
-    map′ (uncurry (cong₂ _∷_)) ∷-injective (x ≟ᴬ y ×-dec xs ≟ᴸᴬ ys)
+    map′ (uncurry (cong₂ _∷_)) ∷-injective (x ≟ᴬ y ×? xs ≟ᴸᴬ ys)
 
 -- The final case says that `x ∷ xs ≡ y ∷ ys` exactly when `x ≡ y` *and*
 -- `xs ≡ ys`. The proofs are updated by the first two arguments to `map′`.
 
 -- In the case of ≡-equality tests, the pattern
--- `map′ (congₙ c) c-injective (x₀ ≟ y₀ ×-dec ... ×-dec xₙ₋₁ ≟ yₙ₋₁)`
+-- `map′ (congₙ c) c-injective (x₀ ≟ y₀ ×? ... ×? xₙ₋₁ ≟ yₙ₋₁)`
 -- is captured by `≟-mapₙ n c c-injective (x₀ ≟ y₀) ... (xₙ₋₁ ≟ yₙ₋₁)`.
 
 module ListDecEq₁ {a} {A : Set a} (_≟ᴬ_ : (x y : A) → Dec (x ≡ y)) where

src/Data/Fin/Properties.agda

@@ -48,7 +48,7 @@ open import Relation.Binary.PropositionalEquality.Properties as ≡
 open import Relation.Binary.PropositionalEquality as ≡
   using (≡-≟-identity; ≢-≟-identity)
 open import Relation.Nullary.Decidable as Dec
-  using (Dec; _because_; yes; no; _×-dec_; _⊎-dec_; map′)
+  using (Dec; _because_; yes; no; _×?_; _⊎?_; map′)
 open import Relation.Nullary.Negation.Core
   using (¬_; contradiction; contradiction′)
 open import Relation.Nullary.Reflects using (invert)
@@ -1021,11 +1021,11 @@ module _ {P : Pred (Fin (suc n)) p} where
 
 any? : ∀ {P : Pred (Fin n) p} → Decidable P → Dec (∃ P)
 any? {zero}  P? = no λ{ (() , _) }
-any? {suc _} P? = Dec.map ⊎⇔∃ (P? zero ⊎-dec any? (P? ∘ suc))
+any? {suc _} P? = Dec.map ⊎⇔∃ (P? zero ⊎? any? (P? ∘ suc))
 
 all? : ∀ {P : Pred (Fin n) p} → Decidable P → Dec (∀ i → P i)
 all? {zero}  P? = yes λ()
-all? {suc _} P? = Dec.map ∀-cons-⇔ (P? zero ×-dec all? (P? ∘ suc))
+all? {suc _} P? = Dec.map ∀-cons-⇔ (P? zero ×? all? (P? ∘ suc))
 
 private
   -- A nice computational property of `all?`:
@@ -1076,7 +1076,7 @@ decFinSubset {suc _} {P = P} {Q = Q} Q? P? = dec[Q⊆P]
   dec[Q⊆P] : Dec (Q ⊆ P)
   dec[Q⊆P] with Q? zero
   ... | no ¬q₀ = map′ (cons (contradiction′ ¬q₀)) Q⊆P⇒Q⊆ₛP ih
-  ... | yes q₀ = map′ (uncurry (cons ∘ const)) < _$ q₀ , Q⊆P⇒Q⊆ₛP > (P? q₀ ×-dec ih)
+  ... | yes q₀ = map′ (uncurry (cons ∘ const)) < _$ q₀ , Q⊆P⇒Q⊆ₛP > (P? q₀ ×? ih)
 
 ------------------------------------------------------------------------
 -- Properties of functions to and from Fin
@@ -1120,7 +1120,7 @@ cantor-schröder-bernstein f-inj g-inj = ℕ.≤-antisym
 injective⇒existsPivot : ∀ {f : Fin n → Fin m} → Injective _≡_ _≡_ f →
                         ∀ (i : Fin n) → ∃ λ j → j ≤ i × i ≤ f j
 injective⇒existsPivot {f = f} f-injective i
-  with any? (λ j → j ≤? i ×-dec i ≤? f j)
+  with any? (λ j → j ≤? i ×? i ≤? f j)
 ... | yes result = result
 ... | no ¬result = contradiction′ notInjective-Fin[1+n]→Fin[n] f∘inject!-injective
   where

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 ∷_)))
 
 
 

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

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)

src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda

@@ -23,7 +23,7 @@ open import Data.Nat.Base using (zero; suc; _≤_)
 import Data.Nat.Properties as ℕ
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (case_of_; _$′_)
-open import Relation.Nullary.Decidable using (yes; no; does; map′; _⊎-dec_)
+open import Relation.Nullary.Decidable using (yes; no; does; map′; _⊎?_)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary.Core using (REL; _⇒_)
@@ -167,4 +167,4 @@ infix? R? [] [] = yes (here [])
 infix? R? (a ∷ as) [] = no (λ where (here ()))
 infix? R? as bbs@(_ ∷ bs) =
   map′ [ here , there ]′ ∷⁻
-  (Prefix.prefix? R? as bbs ⊎-dec infix? R? as bs)
+  (Prefix.prefix? R? as bbs ⊎? infix? R? as bs)

src/Data/List/Relation/Binary/Lex.agda

@@ -19,7 +19,7 @@ open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (_⊔_)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Decidable as Dec
-  using (Dec; yes; no; _×-dec_; _⊎-dec_)
+  using (Dec; yes; no; _×?_; _⊎?_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Structures using (IsEquivalence)
 open import Relation.Binary.Definitions
@@ -116,4 +116,4 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} {P : Set}
     decidable []       (y ∷ ys) = yes halt
     decidable (x ∷ xs) []       = no λ()
     decidable (x ∷ xs) (y ∷ ys) =
-      Dec.map ∷<∷-⇔ (dec-≺ x y ⊎-dec (dec-≈ x y ×-dec decidable xs ys))
+      Dec.map ∷<∷-⇔ (dec-≺ x y ⊎? (dec-≈ x y ×? decidable xs ys))

src/Data/List/Relation/Binary/Pointwise/Properties.agda

@@ -16,7 +16,7 @@ open import Level
 open import Relation.Binary.Core using (REL; _⇒_)
 open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-open import Relation.Nullary using (yes; no; _×-dec_)
+open import Relation.Nullary using (yes; no; _×?_)
 import Relation.Nullary.Decidable as Dec
 
 open import Data.List.Relation.Binary.Pointwise.Base
@@ -71,7 +71,7 @@ decidable _  []       []       = yes []
 decidable _  []       (y ∷ ys) = no λ()
 decidable _  (x ∷ xs) []       = no λ()
 decidable R? (x ∷ xs) (y ∷ ys) = Dec.map′ (uncurry _∷_) uncons
-  (R? x y ×-dec decidable R? xs ys)
+  (R? x y ×? decidable R? xs ys)
 
 irrelevant : Irrelevant R → Irrelevant (Pointwise R)
 irrelevant irr []       []         = ≡.refl

src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda

@@ -28,7 +28,7 @@ open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl; cong₂)
 open import Relation.Nullary.Decidable.Core as Dec
-  using (_×-dec_; yes; no; _because_)
+  using (_×?_; yes; no; _because_)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Unary as U using (Pred)
 
@@ -221,4 +221,4 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
   prefix? R? []       bs       = yes []
   prefix? R? (a ∷ as) []       = no (λ ())
   prefix? R? (a ∷ as) (b ∷ bs) = Dec.map′ (uncurry _∷_) uncons
-                               $ R? a b ×-dec prefix? R? as bs
+                               $ R? a b ×? prefix? R? as bs

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

@@ -20,7 +20,7 @@ open import Effect.Monad
 open import Function.Base using (_∘_; _∘′_; id; const)
 open import Level using (Level; _⊔_)
 open import Relation.Nullary.Decidable.Core as Dec
-  using (_×-dec_; yes; no; map′)
+  using (_×?_; yes; no; map′)
 open import Relation.Unary hiding (_∈_)
 import Relation.Unary.Properties as Unary
 open import Relation.Binary.Bundles using (Setoid)
@@ -206,7 +206,7 @@ module _(S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) 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? p (x ∷ xs) = Dec.map′ (uncurry _∷_) uncons (p x ×? all? p xs)
 
 universal : Universal P → Universal (All P)
 universal u []       = []

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

@@ -20,7 +20,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 (_×-dec_; yes; no)
+open import Relation.Nullary.Decidable as Dec using (_×?_; yes; no)
 
 ------------------------------------------------------------------------
 -- Definition
@@ -69,7 +69,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 ×? allPairs? R? xs)
 
 irrelevant : B.Irrelevant R → U.Irrelevant (AllPairs R)
 irrelevant irr []           []           = refl

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

@@ -13,7 +13,7 @@ open import Data.List.Base as List using (List; []; [_]; _∷_; removeAt)
 open import Data.Product.Base as Product using (∃; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary.Decidable.Core as Dec using (no; _⊎-dec_)
+open import Relation.Nullary.Decidable.Core as Dec using (no; _⊎?_)
 open import Relation.Nullary.Negation using (¬_; contradiction)
 open import Relation.Unary using (Pred; _⊆_; Decidable; Satisfiable)
 
@@ -88,7 +88,7 @@ fromSum (inj₂ pxs) = there pxs
 
 any? : Decidable P → Decidable (Any P)
 any? P? []       = no λ()
-any? P? (x ∷ xs) = Dec.map′ fromSum toSum (P? x ⊎-dec any? P? xs)
+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

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]

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

@@ -22,7 +22,7 @@ open import Relation.Binary.Core using (Rel; _⇒_)
 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 using (yes; no; map′; _×-dec_)
+open import Relation.Nullary.Decidable using (yes; no; map′; _×?_)
 
 private
   variable
@@ -111,7 +111,7 @@ module _ {R : Rel A ℓ} where
   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)
   irrelevant irr []           []           = refl

src/Data/Nat/Primality.agda

@@ -21,7 +21,7 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (flip; _∘_; _∘′_)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Relation.Nullary.Decidable as Dec
-  using (yes; no; from-yes; from-no; ¬?; _×-dec_; _⊎-dec_; _→-dec_; decidable-stable)
+  using (yes; no; from-yes; from-no; ¬?; _×?_; _⊎?_; _→?_; decidable-stable)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction; contradiction₂)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Binary.Core using (Rel)
@@ -194,7 +194,7 @@ composite? n = Dec.map CompositeUpTo⇔Composite (compositeUpTo? n)
 
   -- Proof of decidability
   compositeUpTo? : Decidable CompositeUpTo
-  compositeUpTo? n = anyUpTo? (λ d → nonTrivial? d ×-dec d ∣? n) n
+  compositeUpTo? n = anyUpTo? (λ d → nonTrivial? d ×? d ∣? n) n
 
 ------------------------------------------------------------------------
 -- Primality
@@ -239,7 +239,7 @@ prime? n@(2+ _) = Dec.map PrimeUpTo⇔Prime (primeUpTo? n)
 
   -- Proof of decidability
   primeUpTo? : Decidable PrimeUpTo
-  primeUpTo? n = allUpTo? (λ d → nonTrivial? d →-dec ¬? (d ∣? n)) n
+  primeUpTo? n = allUpTo? (λ d → nonTrivial? d →? ¬? (d ∣? n)) n
 
 -- Euclid's lemma - for p prime, if p ∣ m * n, then either p ∣ m or p ∣ n.
 --
@@ -374,7 +374,7 @@ irreducible? n@(suc _) =
   -- Decidability
   irreducibleUpTo? : Decidable IrreducibleUpTo
   irreducibleUpTo? n = allUpTo?
-    (λ m → (m ∣? n) →-dec (m ≟ 1 ⊎-dec m ≟ n)) n
+    (λ m → (m ∣? n) →? (m ≟ 1 ⊎? m ≟ n)) n
 
 -- Relationship between primality and irreducibility.
 prime⇒irreducible : Prime p → Irreducible p

src/Data/Product/Nary/NonDependent.agda

@@ -22,7 +22,7 @@ open import Data.Nat.Base using (ℕ; zero; suc; pred)
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Unit.Base using (⊤)
 open import Function.Base using (const; _∘′_; _∘_)
-open import Relation.Nullary.Decidable.Core using (Dec; yes; no; _×-dec_)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no; _×?_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
 
@@ -131,12 +131,12 @@ uncurry⊤ₙ (suc n) f = uncurry (uncurry⊤ₙ n ∘′ f)
 
 Product⊤-dec : ∀ n {ls} {as : Sets n ls} → Product⊤ n (Dec <$> as) → Dec (Product⊤ n as)
 Product⊤-dec zero    _          = yes _
-Product⊤-dec (suc n) (p? , ps?) = p? ×-dec Product⊤-dec n ps?
+Product⊤-dec (suc n) (p? , ps?) = p? ×? Product⊤-dec n ps?
 
 Product-dec : ∀ n {ls} {as : Sets n ls} → Product n (Dec <$> as) → Dec (Product n as)
 Product-dec 0               _          = yes _
 Product-dec 1               p?         = p?
-Product-dec (suc n@(suc _)) (p? , ps?) = p? ×-dec Product-dec n ps?
+Product-dec (suc n@(suc _)) (p? , ps?) = p? ×? Product-dec n ps?
 
 ------------------------------------------------------------------------
 -- pointwise liftings

src/Data/Product/Relation/Binary/Lex/Strict.agda

@@ -29,7 +29,7 @@ open import Relation.Binary.Definitions
         ; tri<; tri>; tri≈)
 open import Relation.Binary.Consequences using (asym⇒irr)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-open import Relation.Nullary.Decidable.Core using (yes; no; _⊎-dec_; _×-dec_)
+open import Relation.Nullary.Decidable.Core using (yes; no; _⊎?_; _×?_)
 open import Relation.Nullary.Negation.Core using (contradiction)
 
 private
@@ -111,9 +111,9 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂} {_<₂_ : Rel B ℓ
                 Decidable _<ₗₑₓ_
   ×-decidable dec-≈₁ dec-<₁ dec-≤₂ x y =
     dec-<₁ (proj₁ x) (proj₁ y)
-      ⊎-dec
+      ⊎?
     (dec-≈₁ (proj₁ x) (proj₁ y)
-       ×-dec
+       ×?
      dec-≤₂ (proj₂ x) (proj₂ y))
 
 module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂}

src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda

@@ -13,7 +13,7 @@ open import Data.Sum.Base using (inj₁; inj₂)
 open import Level using (Level; _⊔_; 0ℓ)
 open import Function.Base using (id)
 open import Function.Bundles using (Inverse)
-open import Relation.Nullary.Decidable using (_×-dec_)
+open import Relation.Nullary.Decidable using (_×?_)
 open import Relation.Binary.Core using (REL; Rel; _⇒_)
 open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; Preorder; Poset; StrictPartialOrder)
@@ -88,7 +88,7 @@ Pointwise R S (a , c) (b , d) = (R a b) × (S c d)
 ... | inj₂ y₁∼x₁ | inj₁ x₂∼y₂ = inj₁ (sym₁ y₁∼x₁ , x₂∼y₂)
 
 ×-decidable : Decidable R → Decidable S → Decidable (Pointwise R S)
-×-decidable _≟₁_ _≟₂_ (x₁ , x₂) (y₁ , y₂) = (x₁ ≟₁ y₁) ×-dec (x₂ ≟₂ y₂)
+×-decidable _≟₁_ _≟₂_ (x₁ , x₂) (y₁ , y₂) = (x₁ ≟₁ y₁) ×? (x₂ ≟₂ y₂)
 
 ------------------------------------------------------------------------
 -- Structures can also be combined.