From e0bf280af587b7b2a01ede6b0096ae0b6a4e9412 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 26 Oct 2025 09:22:18 +0000 Subject: [PATCH 1/4] refactor: fixes #2842 --- CHANGELOG.md | 9 ++++ src/Relation/Nullary/Decidable/Core.agda | 66 ++++++++++++++++++------ 2 files changed, 58 insertions(+), 17 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0c9486c005..db42254f6d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -53,6 +53,15 @@ Deprecated names interchange ↦ medial ``` +* In `Relation.Nullary.Decidable.Core`: + ```agda + ⊤-dec ↦ ⊤? + ⊥-dec ↦ ⊥? + _×-dec_ ↦ _×?_ + _⊎-dec_ ↦ _⊎?_ + _→-dec_ ↦ _→?_ + ``` + * In `Relation.Nullary.Negation`: ```agda ∃⟶¬∀¬ ↦ ∃⇒¬∀¬ diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda index b964141439..9142aa5887 100644 --- a/src/Relation/Nullary/Decidable/Core.agda +++ b/src/Relation/Nullary/Decidable/Core.agda @@ -91,8 +91,8 @@ recompute-irrelevant-id = Recomputable.recompute-irrelevant-id ∘ recompute ------------------------------------------------------------------------ -- Interaction with negation, sum, product etc. -infixr 1 _⊎-dec_ -infixr 2 _×-dec_ _→-dec_ +infixr 1 _⊎?_ +infixr 2 _×?_ _→?_ T? : ∀ x → Dec (T x) T? x = x because T-reflects x @@ -101,25 +101,25 @@ T? x = x because T-reflects x does (¬? a?) = not (does a?) proof (¬? a?) = ¬-reflects (proof a?) -⊤-dec : Dec {a} ⊤ -does ⊤-dec = true -proof ⊤-dec = ⊤-reflects +⊤? : Dec {a} ⊤ +does ⊤? = true +proof ⊤? = ⊤-reflects -_×-dec_ : Dec A → Dec B → Dec (A × B) -does (a? ×-dec b?) = does a? ∧ does b? -proof (a? ×-dec b?) = proof a? ×-reflects proof b? +_×?_ : Dec A → Dec B → Dec (A × B) +does (a? ×? b?) = does a? ∧ does b? +proof (a? ×? b?) = proof a? ×-reflects proof b? -⊥-dec : Dec {a} ⊥ -does ⊥-dec = false -proof ⊥-dec = ⊥-reflects +⊥? : Dec {a} ⊥ +does ⊥? = false +proof ⊥? = ⊥-reflects -_⊎-dec_ : Dec A → Dec B → Dec (A ⊎ B) -does (a? ⊎-dec b?) = does a? ∨ does b? -proof (a? ⊎-dec b?) = proof a? ⊎-reflects proof b? +_⊎?_ : Dec A → Dec B → Dec (A ⊎ B) +does (a? ⊎? b?) = does a? ∨ does b? +proof (a? ⊎? b?) = proof a? ⊎-reflects proof b? -_→-dec_ : Dec A → Dec B → Dec (A → B) -does (a? →-dec b?) = not (does a?) ∨ does b? -proof (a? →-dec b?) = proof a? →-reflects proof b? +_→?_ : Dec A → Dec B → Dec (A → B) +does (a? →? b?) = not (does a?) ∨ does b? +proof (a? →? b?) = proof a? →-reflects proof b? ------------------------------------------------------------------------ -- Relationship with Maybe @@ -257,3 +257,35 @@ toDec = fromSum "Warning: toDec was deprecated in v2.1. Please use Relation.Nullary.Decidable.Core.fromSum instead." #-} + +-- Version 2.4 + +infixr 1 _⊎-dec_ +infixr 2 _×-dec_ _→-dec_ + +⊤-dec = ⊤? +{-# WARNING_ON_USAGE ⊤-dec +"Warning: ⊤-dec was deprecated in v2.4. +Please use Relation.Nullary.Decidable.Core.⊤? instead." +#-} +⊥-dec = ⊥? +{-# WARNING_ON_USAGE ⊥-dec +"Warning: ⊥-dec was deprecated in v2.4. +Please use Relation.Nullary.Decidable.Core.⊥? instead." +#-} +_×-dec_ = _×?_ +{-# WARNING_ON_USAGE _×-dec_ +"Warning: _×-dec_ was deprecated in v2.4. +Please use Relation.Nullary.Decidable.Core._×?_ instead." +#-} +_⊎-dec_ = _⊎?_ +{-# WARNING_ON_USAGE _⊎-dec_ +"Warning: _⊎-dec_ was deprecated in v2.4. +Please use Relation.Nullary.Decidable.Core._⊎?_ instead." +#-} +_→-dec_ = _→?_ +{-# WARNING_ON_USAGE _→-dec_ +"Warning: _→-dec_ was deprecated in v2.4. +Please use Relation.Nullary.Decidable.Core._→?_ instead." +#-} + From 0786e8fda49bce36adffe200103bac70448e9c50 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 26 Oct 2025 09:59:02 +0000 Subject: [PATCH 2/4] refactor: knock-ons --- doc/README/Design/Decidability.agda | 8 +++---- src/Data/Fin/Properties.agda | 8 +++---- .../Infix/Heterogeneous/Properties.agda | 4 ++-- src/Data/List/Relation/Binary/Lex.agda | 4 ++-- .../Relation/Binary/Pointwise/Properties.agda | 4 ++-- .../Prefix/Heterogeneous/Properties.agda | 4 ++-- src/Data/List/Relation/Unary/All.agda | 4 ++-- src/Data/List/Relation/Unary/AllPairs.agda | 4 ++-- src/Data/List/Relation/Unary/Any.agda | 4 ++-- src/Data/List/Relation/Unary/Linked.agda | 4 ++-- src/Data/Nat/Primality.agda | 8 +++---- src/Data/Product/Nary/NonDependent.agda | 6 ++--- .../Product/Relation/Binary/Lex/Strict.agda | 6 ++--- .../Binary/Pointwise/NonDependent.agda | 4 ++-- src/Data/Vec/Properties.agda | 4 ++-- src/Data/Vec/Relation/Unary/All.agda | 4 ++-- src/Data/Vec/Relation/Unary/Any.agda | 4 ++-- src/Reflection/AST/Abstraction.agda | 4 ++-- src/Reflection/AST/Argument.agda | 4 ++-- src/Reflection/AST/Argument/Information.agda | 4 ++-- src/Reflection/AST/Argument/Modality.agda | 4 ++-- src/Reflection/AST/Definition.agda | 8 +++---- src/Reflection/AST/Term.agda | 24 +++++++++---------- .../Closure/Reflexive/Properties.agda | 2 +- .../Binary/Construct/Intersection.agda | 4 ++-- .../Binary/Construct/NonStrictToStrict.agda | 4 ++-- src/Relation/Unary/Properties.agda | 10 ++++---- src/Text/Regex/Properties.agda | 8 +++---- 28 files changed, 80 insertions(+), 80 deletions(-) diff --git a/doc/README/Design/Decidability.agda b/doc/README/Design/Decidability.agda index c6f086424f..63ab9f2021 100644 --- a/doc/README/Design/Decidability.agda +++ b/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 diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 2b3e2f1285..eb85c546b5 100644 --- a/src/Data/Fin/Properties.agda +++ b/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) @@ -1030,11 +1030,11 @@ decFinSubset {suc n} {P = P} {Q} Q? P? ... | true because [Q0] | cons = map′ (uncurry λ P0 rec {x} → cons (λ _ → P0) (λ x → rec {x}) x) < _$ invert [Q0] , (λ f {x} → f {suc x}) > - (P? (invert [Q0]) ×-dec decFinSubset (Q? ∘ suc) P?) + (P? (invert [Q0]) ×? decFinSubset (Q? ∘ suc) P?) any? : ∀ {p} {P : Pred (Fin n) p} → Decidable P → Dec (∃ P) any? {zero} {P = _} P? = no λ { (() , _) } -any? {suc n} {P = P} P? = Dec.map ⊎⇔∃ (P? zero ⊎-dec any? (P? ∘ suc)) +any? {suc n} {P = P} P? = Dec.map ⊎⇔∃ (P? zero ⊎? any? (P? ∘ suc)) all? : ∀ {p} {P : Pred (Fin n) p} → Decidable P → Dec (∀ f → P f) all? P? = map′ (λ ∀p f → ∀p tt) (λ ∀p {x} _ → ∀p x) @@ -1109,7 +1109,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 diff --git a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda index 6fd10257d3..55bd9bbf7c 100644 --- a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda +++ b/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) diff --git a/src/Data/List/Relation/Binary/Lex.agda b/src/Data/List/Relation/Binary/Lex.agda index 0cd178d49f..1baaf2a4a0 100644 --- a/src/Data/List/Relation/Binary/Lex.agda +++ b/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)) diff --git a/src/Data/List/Relation/Binary/Pointwise/Properties.agda b/src/Data/List/Relation/Binary/Pointwise/Properties.agda index cbbae89a11..8bffe52263 100644 --- a/src/Data/List/Relation/Binary/Pointwise/Properties.agda +++ b/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 diff --git a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda index 9b3e638b1b..599c0e5070 100644 --- a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda +++ b/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 diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda index eb9438fec7..7e964a149c 100644 --- a/src/Data/List/Relation/Unary/All.agda +++ b/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 [] = [] diff --git a/src/Data/List/Relation/Unary/AllPairs.agda b/src/Data/List/Relation/Unary/AllPairs.agda index 6036586822..3fe65f7c3f 100644 --- a/src/Data/List/Relation/Unary/AllPairs.agda +++ b/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 diff --git a/src/Data/List/Relation/Unary/Any.agda b/src/Data/List/Relation/Unary/Any.agda index 361cbb4160..b43a84bb7b 100644 --- a/src/Data/List/Relation/Unary/Any.agda +++ b/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 diff --git a/src/Data/List/Relation/Unary/Linked.agda b/src/Data/List/Relation/Unary/Linked.agda index 6717adebd0..24ec966af4 100644 --- a/src/Data/List/Relation/Unary/Linked.agda +++ b/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 diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index c70cc5c3bc..cde58dc602 100644 --- a/src/Data/Nat/Primality.agda +++ b/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 diff --git a/src/Data/Product/Nary/NonDependent.agda b/src/Data/Product/Nary/NonDependent.agda index a698e56bc6..8ef83ed18a 100644 --- a/src/Data/Product/Nary/NonDependent.agda +++ b/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 diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda index 6fa2ab6711..b864f7c3a5 100644 --- a/src/Data/Product/Relation/Binary/Lex/Strict.agda +++ b/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 ℓ₂} diff --git a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda index 5e1c5c5c80..20a1d5ce01 100644 --- a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda +++ b/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. diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 2ca7beb514..93c376b6ce 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -36,7 +36,7 @@ open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning) open import Relation.Unary using (Pred; Decidable) open import Relation.Nullary.Decidable.Core - using (Dec; does; yes; _×-dec_; map′) + using (Dec; does; yes; _×?_; map′) open import Relation.Nullary.Negation.Core using (contradiction) import Data.Nat.GeneralisedArithmetic as ℕ @@ -76,7 +76,7 @@ toList-injective m≡n (x ∷ xs) (y ∷ ys) xs=ys = ≡-dec : DecidableEquality A → DecidableEquality (Vec A n) ≡-dec _≟_ [] [] = yes refl ≡-dec _≟_ (x ∷ xs) (y ∷ ys) = map′ (uncurry (cong₂ _∷_)) - ∷-injective (x ≟ y ×-dec ≡-dec _≟_ xs ys) + ∷-injective (x ≟ y ×? ≡-dec _≟_ xs ys) ------------------------------------------------------------------------ -- _[_]=_ diff --git a/src/Data/Vec/Relation/Unary/All.agda b/src/Data/Vec/Relation/Unary/All.agda index 1c20d9c478..4f7022550c 100644 --- a/src/Data/Vec/Relation/Unary/All.agda +++ b/src/Data/Vec/Relation/Unary/All.agda @@ -17,7 +17,7 @@ open import Data.Vec.Membership.Propositional renaming (_∈_ to _∈ₚ_) import Data.Vec.Membership.Setoid as SetoidMembership open import Function.Base using (_∘_) open import Level using (Level; _⊔_) -open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no) +open import Relation.Nullary.Decidable as Dec using (_×?_; yes; no) open import Relation.Unary hiding (_∈_) open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Definitions using (_Respects_) @@ -108,7 +108,7 @@ module _(S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) 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? P? (x ∷ xs) = Dec.map′ (uncurry _∷_) uncons (P? x ×? all? P? xs) universal : Universal P → ∀ {n} → Universal (All P {n}) universal u [] = [] diff --git a/src/Data/Vec/Relation/Unary/Any.agda b/src/Data/Vec/Relation/Unary/Any.agda index bf30b01076..157d275cf9 100644 --- a/src/Data/Vec/Relation/Unary/Any.agda +++ b/src/Data/Vec/Relation/Unary/Any.agda @@ -15,7 +15,7 @@ open import Data.Vec.Base as Vec using (Vec; []; [_]; _∷_) open import Data.Product.Base as Product using (∃; _,_) open import Level using (Level; _⊔_) open import Relation.Nullary.Negation using (¬_; contradiction) -open import Relation.Nullary.Decidable as Dec using (no; _⊎-dec_) +open import Relation.Nullary.Decidable as Dec using (no; _⊎?_) open import Relation.Unary private @@ -75,7 +75,7 @@ satisfied (there pxs) = satisfied pxs any? : Decidable P → ∀ {n} → Decidable (Any P {n}) 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 → ∀ {n} → Satisfiable (Any P {suc n}) satisfiable (x , p) {zero} = x ∷ [] , here p diff --git a/src/Reflection/AST/Abstraction.agda b/src/Reflection/AST/Abstraction.agda index 2f19e5c8b6..e91ae8d00c 100644 --- a/src/Reflection/AST/Abstraction.agda +++ b/src/Reflection/AST/Abstraction.agda @@ -12,7 +12,7 @@ open import Data.String.Base as String using (String) open import Data.String.Properties as String using (_≟_) open import Data.Product.Base using (_×_; <_,_>; uncurry) open import Level using (Level) -open import Relation.Nullary.Decidable.Core using (Dec; map′; _×-dec_) +open import Relation.Nullary.Decidable.Core using (Dec; map′; _×?_) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂) @@ -59,7 +59,7 @@ unAbs (abs s a) = a unAbs-dec : {abs1 abs2 : Abs A} → Dec (unAbs abs1 ≡ unAbs abs2) → Dec (abs1 ≡ abs2) unAbs-dec {abs1 = abs s a} {abs t a′} a≟a′ = - map′ (uncurry (cong₂ abs)) abs-injective (s String.≟ t ×-dec a≟a′) + map′ (uncurry (cong₂ abs)) abs-injective (s String.≟ t ×? a≟a′) ≡-dec : DecidableEquality A → DecidableEquality (Abs A) ≡-dec _≟_ x y = unAbs-dec (unAbs x ≟ unAbs y) diff --git a/src/Reflection/AST/Argument.agda b/src/Reflection/AST/Argument.agda index 2ffc41309f..9fd29e7330 100644 --- a/src/Reflection/AST/Argument.agda +++ b/src/Reflection/AST/Argument.agda @@ -10,7 +10,7 @@ module Reflection.AST.Argument where open import Data.List.Base as List using (List; []; _∷_) open import Data.Product.Base using (_×_; <_,_>; uncurry) -open import Relation.Nullary.Decidable.Core using (Dec; map′; _×-dec_) +open import Relation.Nullary.Decidable.Core using (Dec; map′; _×?_) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂) open import Level using (Level) @@ -86,7 +86,7 @@ unArg (arg i a) = a unArg-dec : {arg1 arg2 : Arg A} → Dec (unArg arg1 ≡ unArg arg2) → Dec (arg1 ≡ arg2) unArg-dec {arg1 = arg i x} {arg j y} arg1≟arg2 = - map′ (uncurry (cong₂ arg)) arg-injective (i Information.≟ j ×-dec arg1≟arg2) + map′ (uncurry (cong₂ arg)) arg-injective (i Information.≟ j ×? arg1≟arg2) ≡-dec : DecidableEquality A → DecidableEquality (Arg A) ≡-dec _≟_ x y = unArg-dec (unArg x ≟ unArg y) diff --git a/src/Reflection/AST/Argument/Information.agda b/src/Reflection/AST/Argument/Information.agda index 3aba388215..307a1b1976 100644 --- a/src/Reflection/AST/Argument/Information.agda +++ b/src/Reflection/AST/Argument/Information.agda @@ -9,7 +9,7 @@ module Reflection.AST.Argument.Information where open import Data.Product.Base using (_×_; <_,_>; uncurry) -open import Relation.Nullary.Decidable.Core using (map′; _×-dec_) +open import Relation.Nullary.Decidable.Core using (map′; _×?_) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂) open import Reflection.AST.Argument.Modality as Modality using (Modality) @@ -54,4 +54,4 @@ arg-info v m ≟ arg-info v′ m′ = map′ (uncurry (cong₂ arg-info)) arg-info-injective - (v Visibility.≟ v′ ×-dec m Modality.≟ m′) + (v Visibility.≟ v′ ×? m Modality.≟ m′) diff --git a/src/Reflection/AST/Argument/Modality.agda b/src/Reflection/AST/Argument/Modality.agda index d5f084e5d1..e71b0f2710 100644 --- a/src/Reflection/AST/Argument/Modality.agda +++ b/src/Reflection/AST/Argument/Modality.agda @@ -9,7 +9,7 @@ module Reflection.AST.Argument.Modality where open import Data.Product.Base using (_×_; <_,_>; uncurry) -open import Relation.Nullary.Decidable.Core using (map′; _×-dec_) +open import Relation.Nullary.Decidable.Core using (map′; _×?_) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂) open import Reflection.AST.Argument.Relevance as Relevance using (Relevance) @@ -54,4 +54,4 @@ modality r q ≟ modality r′ q′ = map′ (uncurry (cong₂ modality)) modality-injective - (r Relevance.≟ r′ ×-dec q Quantity.≟ q′) + (r Relevance.≟ r′ ×? q Quantity.≟ q′) diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda index 1d3f10f1c0..400499afd3 100644 --- a/src/Reflection/AST/Definition.agda +++ b/src/Reflection/AST/Definition.agda @@ -11,7 +11,7 @@ module Reflection.AST.Definition where import Data.List.Properties as List using (≡-dec) import Data.Nat.Properties as ℕ using (_≟_) open import Data.Product.Base using (_×_; <_,_>; uncurry) -open import Relation.Nullary.Decidable.Core using (map′; _×-dec_; yes; no) +open import Relation.Nullary.Decidable.Core using (map′; _×?_; yes; no) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂) import Reflection.AST.Argument as Arg using (Arg; ≡-dec) @@ -72,13 +72,13 @@ function cs ≟ function cs′ = map′ (cong function) function-injective (cs Term.≟-Clauses cs′) data-type pars cs ≟ data-type pars′ cs′ = map′ (uncurry (cong₂ data-type)) data-type-injective - (pars ℕ.≟ pars′ ×-dec List.≡-dec Name._≟_ cs cs′) + (pars ℕ.≟ pars′ ×? List.≡-dec Name._≟_ cs cs′) record′ c fs ≟ record′ c′ fs′ = map′ (uncurry (cong₂ record′)) record′-injective - (c Name.≟ c′ ×-dec List.≡-dec (Arg.≡-dec Name._≟_) fs fs′) + (c Name.≟ c′ ×? List.≡-dec (Arg.≡-dec Name._≟_) fs fs′) constructor′ d q ≟ constructor′ d′ q′ = map′ (uncurry (cong₂ constructor′)) constructor′-injective - (d Name.≟ d′ ×-dec q Quantity.≟ q′) + (d Name.≟ d′ ×? q Quantity.≟ q′) axiom ≟ axiom = yes refl primitive′ ≟ primitive′ = yes refl diff --git a/src/Reflection/AST/Term.agda b/src/Reflection/AST/Term.agda index 2e7ce98b13..0a1b9e3b53 100644 --- a/src/Reflection/AST/Term.agda +++ b/src/Reflection/AST/Term.agda @@ -17,7 +17,7 @@ open import Data.Product.Properties using (,-injective) open import Data.Maybe.Base using (Maybe; just; nothing) open import Data.String.Base using (String) open import Data.String.Properties as String hiding (_≟_) -open import Relation.Nullary.Decidable using (map′; _×-dec_; yes; no) +open import Relation.Nullary.Decidable using (map′; _×?_; yes; no) open import Relation.Binary.Definitions using (Decidable; DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂) open import Reflection.AST.Abstraction using (Abs; abs; unAbs-dec) @@ -166,7 +166,7 @@ arg i a ≟-ArgType arg i′ a′ = unArg-dec (a ≟ a′) _≟-Telescope_ : DecidableEquality Telescope [] ≟-Telescope [] = yes refl ((x , t) ∷ tel) ≟-Telescope ((x′ , t′) ∷ tel′) = ∷-dec - (map′ (uncurry (cong₂ _,_)) ,-injective ((x String.≟ x′) ×-dec (t ≟-ArgTerm t′))) + (map′ (uncurry (cong₂ _,_)) ,-injective ((x String.≟ x′) ×? (t ≟-ArgTerm t′))) (tel ≟-Telescope tel′) [] ≟-Telescope (_ ∷ _) = no λ () (_ ∷ _) ≟-Telescope [] = no λ () @@ -174,11 +174,11 @@ _≟-Telescope_ : DecidableEquality Telescope clause tel ps b ≟-Clause clause tel′ ps′ b′ = map′ (λ (tel≡tel′ , ps≡ps′ , b≡b′) → cong₂ (uncurry clause) (cong₂ _,_ tel≡tel′ ps≡ps′) b≡b′) clause-injective - (tel ≟-Telescope tel′ ×-dec ps ≟-Patterns ps′ ×-dec b ≟ b′) + (tel ≟-Telescope tel′ ×? ps ≟-Patterns ps′ ×? b ≟ b′) absurd-clause tel ps ≟-Clause absurd-clause tel′ ps′ = map′ (uncurry (cong₂ absurd-clause)) absurd-clause-injective - (tel ≟-Telescope tel′ ×-dec ps ≟-Patterns ps′) + (tel ≟-Telescope tel′ ×? ps ≟-Patterns ps′) clause _ _ _ ≟-Clause absurd-clause _ _ = no λ() absurd-clause _ _ ≟-Clause clause _ _ _ = no λ() @@ -267,19 +267,19 @@ inf-injective : ∀ {x y} → inf x ≡ inf y → x ≡ y inf-injective refl = refl var x args ≟ var x′ args′ = - map′ (uncurry (cong₂ var)) var-injective (x ℕ.≟ x′ ×-dec args ≟-Args args′) + map′ (uncurry (cong₂ var)) var-injective (x ℕ.≟ x′ ×? args ≟-Args args′) con c args ≟ con c′ args′ = - map′ (uncurry (cong₂ con)) con-injective (c Name.≟ c′ ×-dec args ≟-Args args′) + map′ (uncurry (cong₂ con)) con-injective (c Name.≟ c′ ×? args ≟-Args args′) def f args ≟ def f′ args′ = - map′ (uncurry (cong₂ def)) def-injective (f Name.≟ f′ ×-dec args ≟-Args args′) + map′ (uncurry (cong₂ def)) def-injective (f Name.≟ f′ ×? args ≟-Args args′) meta x args ≟ meta x′ args′ = - map′ (uncurry (cong₂ meta)) meta-injective (x Meta.≟ x′ ×-dec args ≟-Args args′) + map′ (uncurry (cong₂ meta)) meta-injective (x Meta.≟ x′ ×? args ≟-Args args′) lam v t ≟ lam v′ t′ = - map′ (uncurry (cong₂ lam)) lam-injective (v Visibility.≟ v′ ×-dec t ≟-AbsTerm t′) + map′ (uncurry (cong₂ lam)) lam-injective (v Visibility.≟ v′ ×? t ≟-AbsTerm t′) pat-lam cs args ≟ pat-lam cs′ args′ = - map′ (uncurry (cong₂ pat-lam)) pat-lam-injective (cs ≟-Clauses cs′ ×-dec args ≟-Args args′) + map′ (uncurry (cong₂ pat-lam)) pat-lam-injective (cs ≟-Clauses cs′ ×? args ≟-Args args′) pi t₁ t₂ ≟ pi t₁′ t₂′ = - map′ (uncurry (cong₂ pi)) pi-injective (t₁ ≟-ArgType t₁′ ×-dec t₂ ≟-AbsType t₂′) + map′ (uncurry (cong₂ pi)) pi-injective (t₁ ≟-ArgType t₁′ ×? t₂ ≟-AbsType t₂′) sort s ≟ sort s′ = map′ (cong sort) sort-injective (s ≟-Sort s′) lit l ≟ lit l′ = map′ (cong lit) lit-injective (l Literal.≟ l′) unknown ≟ unknown = yes refl @@ -437,7 +437,7 @@ dot-injective refl = refl absurd-injective : ∀ {x y} → absurd x ≡ absurd y → x ≡ y absurd-injective refl = refl -con c ps ≟-Pattern con c′ ps′ = map′ (uncurry (cong₂ con)) pat-con-injective (c Name.≟ c′ ×-dec ps ≟-Patterns ps′) +con c ps ≟-Pattern con c′ ps′ = map′ (uncurry (cong₂ con)) pat-con-injective (c Name.≟ c′ ×? ps ≟-Patterns ps′) var x ≟-Pattern var x′ = map′ (cong var) pat-var-injective (x ℕ.≟ x′) lit l ≟-Pattern lit l′ = map′ (cong lit) pat-lit-injective (l Literal.≟ l′) proj a ≟-Pattern proj a′ = map′ (cong proj) proj-injective (a Name.≟ a′) diff --git a/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda b/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda index ea6bd34d4e..e6d494889f 100644 --- a/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda +++ b/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda @@ -84,7 +84,7 @@ module _ {_~_ : Rel A ℓ} where ... | tri> _ _ c = inj₂ [ c ] dec : DecidableEquality A → Decidable _~_ → Decidable _~ᵒ_ - dec ≡-dec ~-dec a b = Dec.map ⊎⇔Refl (≡-dec a b Dec.⊎-dec ~-dec a b) + dec ≡? ~? a b = Dec.map ⊎⇔Refl (≡? a b Dec.⊎? ~? a b) decidable : Trichotomous _≡_ _~_ → Decidable _~ᵒ_ decidable ~-tri a b with ~-tri a b diff --git a/src/Relation/Binary/Construct/Intersection.agda b/src/Relation/Binary/Construct/Intersection.agda index 4e33ae3fab..b5dda5737e 100644 --- a/src/Relation/Binary/Construct/Intersection.agda +++ b/src/Relation/Binary/Construct/Intersection.agda @@ -19,7 +19,7 @@ open import Relation.Binary.Structures open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive; Antisymmetric; Decidable; _Respects_ ; _Respectsˡ_; _Respectsʳ_; _Respects₂_; Minimum; Maximum; Irreflexive) -open import Relation.Nullary.Decidable using (yes; no; _×-dec_) +open import Relation.Nullary.Decidable using (yes; no; _×?_) private variable @@ -87,7 +87,7 @@ module _ (≈ : Rel A ℓ₁) (L : Rel A ℓ₂) (R : Rel A ℓ₃) 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 ------------------------------------------------------------------------ -- Structures diff --git a/src/Relation/Binary/Construct/NonStrictToStrict.agda b/src/Relation/Binary/Construct/NonStrictToStrict.agda index df5d467d37..a4744a2fd9 100644 --- a/src/Relation/Binary/Construct/NonStrictToStrict.agda +++ b/src/Relation/Binary/Construct/NonStrictToStrict.agda @@ -15,7 +15,7 @@ open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) open import Data.Sum.Base using (inj₁; inj₂) open import Function.Base using (_∘_; flip) open import Relation.Nullary using (¬_; yes; no) -open import Relation.Nullary.Decidable using (¬?; _×-dec_) +open import Relation.Nullary.Decidable using (¬?; _×?_) open import Relation.Nullary.Negation using (contradiction) open import Relation.Binary.Structures using (IsPartialOrder; IsEquivalence; IsStrictPartialOrder; IsDecPartialOrder @@ -117,7 +117,7 @@ x < y = x ≤ y × x ≉ y ... | inj₂ y≤x = tri> (x≉y ∘ flip antisym y≤x ∘ proj₁) x≉y (y≤x , x≉y ∘ ≈-sym) <-decidable : Decidable _≈_ → Decidable _≤_ → Decidable _<_ -<-decidable _≟_ _≤?_ x y = x ≤? y ×-dec ¬? (x ≟ y) +<-decidable _≟_ _≤?_ x y = x ≤? y ×? ¬? (x ≟ y) ------------------------------------------------------------------------ -- Structures diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda index b16b6702b8..63a75e4cff 100644 --- a/src/Relation/Unary/Properties.agda +++ b/src/Relation/Unary/Properties.agda @@ -18,7 +18,7 @@ open import Relation.Binary.Definitions hiding (Decidable; Universal; Irrelevant; Empty) open import Relation.Binary.PropositionalEquality.Core using (refl; _≗_) open import Relation.Nullary.Decidable as Dec - using (yes; no; _⊎-dec_; _×-dec_; ¬?; map′; does) + using (yes; no; ¬?; map′; does) open import Relation.Nullary.Negation.Core using (¬_) open import Relation.Unary @@ -238,19 +238,19 @@ infixr 6 _∪?_ _∪?_ : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} → Decidable P → Decidable Q → Decidable (P ∪ Q) -_∪?_ P? Q? x = (P? x) ⊎-dec (Q? x) +_∪?_ P? Q? x = (P? x) Dec.⊎? (Q? x) _∩?_ : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} → Decidable P → Decidable Q → Decidable (P ∩ Q) -_∩?_ P? Q? x = (P? x) ×-dec (Q? x) +_∩?_ P? Q? x = (P? x) Dec.×? (Q? x) _×?_ : {P : Pred A ℓ₁} {Q : Pred B ℓ₂} → Decidable P → Decidable Q → Decidable (P ⟨×⟩ Q) -_×?_ P? Q? (a , b) = (P? a) ×-dec (Q? b) +_×?_ P? Q? (a , b) = (P? a) Dec.×? (Q? b) _⊙?_ : {P : Pred A ℓ₁} {Q : Pred B ℓ₂} → Decidable P → Decidable Q → Decidable (P ⟨⊙⟩ Q) -_⊙?_ P? Q? (a , b) = (P? a) ⊎-dec (Q? b) +_⊙?_ P? Q? (a , b) = (P? a) Dec.⊎? (Q? b) _⊎?_ : {P : Pred A ℓ} {Q : Pred B ℓ} → Decidable P → Decidable Q → Decidable (P ⟨⊎⟩ Q) diff --git a/src/Text/Regex/Properties.agda b/src/Text/Regex/Properties.agda index 6b24e0aa16..b384207d7f 100644 --- a/src/Text/Regex/Properties.agda +++ b/src/Text/Regex/Properties.agda @@ -18,7 +18,7 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Function.Base using (_$_) open import Relation.Nullary.Decidable - using (Dec; yes; no; map′; ¬?; _×-dec_; _⊎-dec_) + using (Dec; yes; no; map′; ¬?; _×?_; _⊎?_) open import Relation.Nullary.Negation using (¬_; contradiction) @@ -44,9 +44,9 @@ open import Text.Regex.Properties.Core preorder public []∈? [ rs ] = no (λ ()) []∈? [^ rs ] = no (λ ()) []∈? (e ∣ f) = map′ sum (λ where (sum pr) → pr) - $ ([]∈? e) ⊎-dec ([]∈? f) + $ ([]∈? e) ⊎? ([]∈? f) []∈? (e ∙ f) = map′ (uncurry (prod ([]++ []))) []∈e∙f-inv - $ ([]∈? e) ×-dec ([]∈? f) + $ ([]∈? e) ×? ([]∈? f) []∈? (e ⋆) = yes (star (sum (inj₁ ε))) infix 4 _∈ᴿ?_ _∉ᴿ?_ _∈?ε _∈?[_] _∈?[^_] @@ -54,7 +54,7 @@ infix 4 _∈ᴿ?_ _∉ᴿ?_ _∈?ε _∈?[_] _∈?[^_] _∈ᴿ?_ : Decidable _∈ᴿ_ c ∈ᴿ? [ a ] = map′ [_] (λ where [ eq ] → eq) (c ≟ a) c ∈ᴿ? (lb ─ ub) = map′ (uncurry _─_) (λ where (ge ─ le) → ge , le) - $ (lb ≤? c) ×-dec (c ≤? ub) + $ (lb ≤? c) ×? (c ≤? ub) _∉ᴿ?_ : Decidable _∉ᴿ_ a ∉ᴿ? r = ¬? (a ∈ᴿ? r) From da62f21b658ed8a9ae5ec603ac6816311a5c0c29 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 26 Oct 2025 11:23:44 +0000 Subject: [PATCH 3/4] refactor: more knock-ons --- src/Data/Fin/Subset/Properties.agda | 4 ++-- src/Data/List/Fresh/Relation/Unary/All.agda | 4 ++-- src/Data/List/Fresh/Relation/Unary/Any.agda | 4 ++-- src/Data/List/Relation/Unary/Grouped.agda | 4 ++-- src/Data/These/Properties.agda | 4 ++-- src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda | 4 ++-- src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda | 4 ++-- src/Data/Vec/Functional/Properties.agda | 4 ++-- src/Data/Vec/Relation/Binary/Lex/Core.agda | 4 ++-- src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda | 4 ++-- src/Data/Vec/Relation/Unary/AllPairs.agda | 4 ++-- src/Data/Vec/Relation/Unary/Linked.agda | 4 ++-- src/Relation/Binary/Construct/StrictToNonStrict.agda | 4 ++-- src/Relation/Binary/Construct/Union.agda | 4 ++-- 14 files changed, 28 insertions(+), 28 deletions(-) diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda index ad734fd647..074a4a05b8 100644 --- 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 index adec42eb7a..fffe091c24 100644 --- 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 index 2d33166dd8..e86379f3ac 100644 --- 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 index f10bc1fd32..8ee0d50f0c 100644 --- 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 index 79d35e53a6..cb59ffdc92 100644 --- 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 index ba0aded0a1..d74229569f 100644 --- 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 (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 index 8b366a4798..c103cc7bab 100644 --- 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 index 7223a83db1..a99c54dd1b 100644 --- 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 From 5346ec9e195073145743b78dbe5cab21ff150777 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 26 Oct 2025 14:23:11 +0000 Subject: [PATCH 4/4] refactor: resolve merge conflict following #2793 --- src/Data/Fin/Properties.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 3427b8e164..95de7da56c 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -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