[ fix ] Relation.Nullary.Decidable.Core names for combinators (#2843)

* refactor: fixes #2842

* refactor: knock-ons

* refactor: more knock-ons

* refactor: resolve merge conflict following #2793

Author: jamesmckinna

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′; decidable-stable)
+  using (Dec; _because_; yes; no; _×?_; _⊎?_; map′; decidable-stable)
 open import Relation.Nullary.Negation.Core
   using (¬_; contradiction; contradiction′)
 open import Relation.Nullary.Reflects using (invert)
@@ -1025,11 +1025,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?`:
@@ -1104,7 +1104,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
@@ -1148,7 +1148,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