From eac8e01ef822db9cf0591f179c6bd619b9a0fc34 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 13 Aug 2023 14:40:35 +0100 Subject: [PATCH 01/57] minor additions to `Decidable` and `Reflects`; plus tidied up deprecation warning --- CHANGELOG.md | 17 ++++++++++++++++- src/Relation/Nullary/Decidable/Core.agda | 18 +++++++++++++++++- src/Relation/Nullary/Reflects.agda | 6 +++++- 3 files changed, 38 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5394b704d0..9f127796d9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -676,7 +676,8 @@ Non-backwards compatible changes - `¬-reflects` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Reflects`. - `decidable-stable`, `excluded-middle` and `¬-drop-Dec` have been moved from `Relation.Nullary.Negation` to `Relation.Nullary.Decidable`. - - `fromDec` and `toDec` have been mvoed from `Data.Sum.Base` to `Data.Sum`. + - `excluded-middle` has been deprecated in favour of `¬¬-excluded-middle` + - `fromDec` and `toDec` have been moved from `Data.Sum.Base` to `Data.Sum`. ### Refactoring of the unindexed Functor/Applicative/Monad hiearchy @@ -2790,6 +2791,20 @@ Other minor changes subst₂-removable : subst₂ _∼_ eq₁ eq₂ p ≅ p ``` +* Added new constructors for `Relation.Nullary.Decidable` + ``` + bool⁺ : ∀ b → Dec (T b) + predᵇ⁺ : (p : A → Bool) (x : A) → Dec (T (p x)) + + ``` + (the first is example `README.Design.Decidability.ex₃` + +* Added new constructor for `Relation.Nullary.Reflects` + ``` + T⁺ : ∀ b → Reflects (T b) b + ``` + (this is example `README.Design.Decidability.ex₂` + * Added new definitions in `Relation.Unary`: ``` _≐_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _ diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda index 2d827519d7..54c5c78ddf 100644 --- a/src/Relation/Nullary/Decidable/Core.agda +++ b/src/Relation/Nullary/Decidable/Core.agda @@ -52,6 +52,15 @@ open Dec public pattern yes p = true because ofʸ p pattern no ¬p = false because ofⁿ ¬p +------------------------------------------------------------------------ +-- decision procedures are Decidable + +bool⁺ : ∀ b → Dec (T b) +bool⁺ b = b because (T⁺ b) + +dec : ∀ {a} {A : Set a} (p : A → Bool) (x : A) → Dec (T (p x)) +dec p x = bool⁺ (p x) + ------------------------------------------------------------------------ -- Recompute @@ -179,7 +188,14 @@ decidable-stable (no ¬p) ¬¬p = ⊥-elim (¬¬p ¬p) ¬¬-excluded-middle : DoubleNegation (Dec P) ¬¬-excluded-middle ¬h = ¬h (no (λ p → ¬h (yes p))) -excluded-middle : DoubleNegation (Dec P) +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + excluded-middle = ¬¬-excluded-middle {-# WARNING_ON_USAGE excluded-middle diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda index 66556e8ae6..9e1168438e 100644 --- a/src/Relation/Nullary/Reflects.agda +++ b/src/Relation/Nullary/Reflects.agda @@ -15,7 +15,7 @@ open import Data.Empty open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) open import Level using (Level) -open import Function.Base using (_$_; _∘_; const) +open import Function.Base using (id; _$_; _∘_; const) open import Relation.Nullary.Negation.Core @@ -37,6 +37,10 @@ data Reflects {p} (P : Set p) : Bool → Set p where ------------------------------------------------------------------------ -- Constructors and destructors +T⁺ : ∀ b → Reflects (T b) b +T⁺ true = ofʸ _ +T⁺ false = ofⁿ id + -- These lemmas are intended to be used mostly when `b` is a value, so -- that the `if` expressions have already been evaluated away. -- In this case, `of` works like the relevant constructor (`ofⁿ` or From 7602d714ea19dc9035896bdfe1f72f8cc8cb34bc Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 13 Aug 2023 14:47:51 +0100 Subject: [PATCH 02/57] moved deprecation notice in `CHANGELOG` --- CHANGELOG.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9f127796d9..deaf7c2b77 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -914,9 +914,6 @@ Non-backwards compatible changes lookup : All P xs → (∀ {x} → x ∈ₚ xs → P x) lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x) ``` - * `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to - `¬¬-excluded-middle`. - Major improvements ------------------ @@ -1471,6 +1468,11 @@ Deprecated names invPreorder ↦ converse-preorder ``` +* In `Relation.Nullary.Decidable.Core`: + ``` + excluded-middle` ↦ `¬¬-excluded-middle` + ``` + ### Renamed Data.Erased to Data.Irrelevant * This fixes the fact we had picked the wrong name originally. The erased modality From cdaee5984453d3556405ba6fcaa569f0b1e83f9f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 13 Aug 2023 14:56:34 +0100 Subject: [PATCH 03/57] naming, plus tidying up `CHANGELOG` --- CHANGELOG.md | 2 -- src/Relation/Nullary/Decidable/Core.agda | 4 ++-- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index deaf7c2b77..d58c8aba3f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2799,13 +2799,11 @@ Other minor changes predᵇ⁺ : (p : A → Bool) (x : A) → Dec (T (p x)) ``` - (the first is example `README.Design.Decidability.ex₃` * Added new constructor for `Relation.Nullary.Reflects` ``` T⁺ : ∀ b → Reflects (T b) b ``` - (this is example `README.Design.Decidability.ex₂` * Added new definitions in `Relation.Unary`: ``` diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda index 54c5c78ddf..eb0267da07 100644 --- a/src/Relation/Nullary/Decidable/Core.agda +++ b/src/Relation/Nullary/Decidable/Core.agda @@ -58,8 +58,8 @@ pattern no ¬p = false because ofⁿ ¬p bool⁺ : ∀ b → Dec (T b) bool⁺ b = b because (T⁺ b) -dec : ∀ {a} {A : Set a} (p : A → Bool) (x : A) → Dec (T (p x)) -dec p x = bool⁺ (p x) +predᵇ⁺ : ∀ {a} {A : Set a} (p : A → Bool) (x : A) → Dec (T (p x)) +predᵇ⁺ p x = bool⁺ (p x) ------------------------------------------------------------------------ -- Recompute From d2c59778b2554271f51e10b086848f3a8dc899f7 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 13 Aug 2023 17:51:08 +0100 Subject: [PATCH 04/57] updated `README.Deisgn.Decidability` to use new defns; simplified imports for `Data.Bool.Properties\' --- README/Design/Decidability.agda | 3 +-- src/Data/Bool/Properties.agda | 7 ++----- 2 files changed, 3 insertions(+), 7 deletions(-) diff --git a/README/Design/Decidability.agda b/README/Design/Decidability.agda index c6f086424f..1e0e3f50d5 100644 --- a/README/Design/Decidability.agda +++ b/README/Design/Decidability.agda @@ -37,8 +37,7 @@ ex₁ : (n : ℕ) → Reflects (zero ≡ suc n) false ex₁ n = ofⁿ λ () ex₂ : (b : Bool) → Reflects (T b) b -ex₂ false = ofⁿ id -ex₂ true = ofʸ tt +ex₂ = T⁺ ------------------------------------------------------------------------ -- Dec diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda index 713ad3da34..31e683c5cd 100644 --- a/src/Data/Bool/Properties.agda +++ b/src/Data/Bool/Properties.agda @@ -24,8 +24,7 @@ open import Level using (Level; 0ℓ) open import Relation.Binary hiding (_⇔_) open import Relation.Binary.PropositionalEquality.Core open import Relation.Binary.PropositionalEquality.Properties -open import Relation.Nullary.Reflects using (ofʸ; ofⁿ) -open import Relation.Nullary.Decidable.Core using (True; does; proof; yes; no) +open import Relation.Nullary.Decidable.Core using (True; does; proof; yes; no; bool⁺) import Relation.Unary as U open import Algebra.Definitions {A = Bool} _≡_ @@ -755,9 +754,7 @@ T-irrelevant : U.Irrelevant T T-irrelevant {true} _ _ = refl T? : U.Decidable T -does (T? b) = b -proof (T? true ) = ofʸ _ -proof (T? false) = ofⁿ λ() +T? = bool⁺ T?-diag : ∀ b → T b → True (T? b) T?-diag true _ = _ From b48287fcf868291341344696e75b065877d2f126 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 13 Aug 2023 18:05:30 +0100 Subject: [PATCH 05/57] simplified imports for `Data.Fin.Base\' --- src/Data/Fin/Base.agda | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index b591301ac0..8d14bada65 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -18,8 +18,6 @@ open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′) open import Function.Base using (id; _∘_; _on_; flip) open import Level using (0ℓ) -open import Relation.Nullary.Negation.Core using (contradiction) -open import Relation.Nullary.Decidable.Core using (yes; no; True; toWitness) open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong) open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel) From 4c16bf048de983f0e9d9d7e8da7d313a410e6404 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 13 Aug 2023 18:15:21 +0100 Subject: [PATCH 06/57] simplified imports for `Data.Fin.Properties\' --- src/Data/Fin/Properties.agda | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 2bacfe58ca..a1705979d7 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -38,10 +38,11 @@ open import Level using (Level) open import Relation.Binary as B hiding (Decidable; _⇔_) open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_; module ≡-Reasoning) -open import Relation.Nullary - using (Reflects; ofʸ; ofⁿ; Dec; _because_; does; proof; yes; no; ¬_; _×-dec_; _⊎-dec_; contradiction) -open import Relation.Nullary.Reflects -open import Relation.Nullary.Decidable as Dec using (map′) +open import Relation.Nullary.Decidable.Core + using (Dec; _because_; does; proof; yes; no; _×-dec_; _⊎-dec_; map′) +open import Relation.Nullary.Decidable as Dec using (via-injection) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) +open import Relation.Nullary.Reflects using (Reflects; ofʸ; ofⁿ; invert) open import Relation.Unary as U using (U; Pred; Decidable; _⊆_; Satisfiable; Universal) open import Relation.Unary.Properties using (U?) @@ -1036,7 +1037,7 @@ module _ {ℓ} {S : Setoid a ℓ} (inj : Injection S (≡-setoid n)) where open Setoid S inj⇒≟ : B.Decidable _≈_ - inj⇒≟ = Dec.via-injection inj _≟_ + inj⇒≟ = via-injection inj _≟_ inj⇒decSetoid : DecSetoid a ℓ inj⇒decSetoid = record From 3c2378670222a1a8525d96aa9a45f2a53b309df5 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 13 Aug 2023 18:17:37 +0100 Subject: [PATCH 07/57] further simplified imports for `Data.Fin.Properties\' --- src/Data/Fin/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index a1705979d7..944191fd4c 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -42,7 +42,7 @@ open import Relation.Nullary.Decidable.Core using (Dec; _because_; does; proof; yes; no; _×-dec_; _⊎-dec_; map′) open import Relation.Nullary.Decidable as Dec using (via-injection) open import Relation.Nullary.Negation.Core using (¬_; contradiction) -open import Relation.Nullary.Reflects using (Reflects; ofʸ; ofⁿ; invert) +open import Relation.Nullary.Reflects using (Reflects; invert) open import Relation.Unary as U using (U; Pred; Decidable; _⊆_; Satisfiable; Universal) open import Relation.Unary.Properties using (U?) From 6cb1d0c1726e76ec784c3523eb742a69cd86101e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 13 Aug 2023 18:20:39 +0100 Subject: [PATCH 08/57] further simplified imports for `Data.Fin.Properties\' --- src/Data/Fin/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 944191fd4c..4a6c54b9bb 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -39,10 +39,10 @@ open import Relation.Binary as B hiding (Decidable; _⇔_) open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_; module ≡-Reasoning) open import Relation.Nullary.Decidable.Core - using (Dec; _because_; does; proof; yes; no; _×-dec_; _⊎-dec_; map′) + using (Dec; _because_; does; yes; no; _×-dec_; _⊎-dec_; map′) open import Relation.Nullary.Decidable as Dec using (via-injection) open import Relation.Nullary.Negation.Core using (¬_; contradiction) -open import Relation.Nullary.Reflects using (Reflects; invert) +open import Relation.Nullary.Reflects using (invert) open import Relation.Unary as U using (U; Pred; Decidable; _⊆_; Satisfiable; Universal) open import Relation.Unary.Properties using (U?) From c99911e0e21b8d53db8c73b47a9cfe340508b437 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 13 Aug 2023 22:48:23 +0100 Subject: [PATCH 09/57] simplified imports for `Data.Integer.*\' --- src/Data/Integer/DivMod.agda | 1 - src/Data/Integer/Divisibility/Signed.agda | 5 ++--- src/Data/Integer/Properties.agda | 25 +++++++++++------------ 3 files changed, 14 insertions(+), 17 deletions(-) diff --git a/src/Data/Integer/DivMod.agda b/src/Data/Integer/DivMod.agda index 87bbaabbe7..4c2846f160 100644 --- a/src/Data/Integer/DivMod.agda +++ b/src/Data/Integer/DivMod.agda @@ -15,7 +15,6 @@ import Data.Nat.Properties as ℕ import Data.Nat.DivMod as ℕ import Data.Sign as S open import Function.Base using (_∘′_) -open import Relation.Nullary.Decidable open import Relation.Binary.PropositionalEquality open ≤-Reasoning diff --git a/src/Data/Integer/Divisibility/Signed.agda b/src/Data/Integer/Divisibility/Signed.agda index db80bcb3a0..4d1cbd6406 100644 --- a/src/Data/Integer/Divisibility/Signed.agda +++ b/src/Data/Integer/Divisibility/Signed.agda @@ -24,8 +24,7 @@ open import Level open import Relation.Binary open import Relation.Binary.PropositionalEquality import Relation.Binary.Reasoning.Preorder as PreorderReasoning -open import Relation.Nullary.Decidable using (yes; no) -import Relation.Nullary.Decidable as DEC +open import Relation.Nullary.Decidable.Core using (yes; no; map′) ------------------------------------------------------------------------ -- Type @@ -130,7 +129,7 @@ module ∣-Reasoning where infix 4 _∣?_ _∣?_ : Decidable _∣_ -k ∣? m = DEC.map′ ∣ᵤ⇒∣ ∣⇒∣ᵤ (∣ k ∣ ℕ.∣? ∣ m ∣) +k ∣? m = map′ ∣ᵤ⇒∣ ∣⇒∣ᵤ (∣ k ∣ ℕ.∣? ∣ m ∣) 0∣⇒≡0 : ∀ {m} → 0ℤ ∣ m → m ≡ 0ℤ 0∣⇒≡0 0|m = ∣i∣≡0⇒i≡0 (ℕ.0∣⇒≡0 (∣⇒∣ᵤ 0|m)) diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 78011e54b1..7a5a54aedd 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -29,10 +29,9 @@ open import Function.Base using (_∘_; _$_; id) open import Level using (0ℓ) open import Relation.Binary open import Relation.Binary.PropositionalEquality -open import Relation.Nullary using (yes; no; ¬_) -import Relation.Nullary.Reflects as Reflects -open import Relation.Nullary.Negation using (contradiction) -import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Decidable.Core using (yes; no; map′) +open import Relation.Nullary.Reflects using (invert) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Algebra.Definitions {A = ℤ} _≡_ open import Algebra.Consequences.Propositional @@ -62,10 +61,10 @@ private infix 4 _≟_ _≟_ : DecidableEquality ℤ -+ m ≟ + n = Dec.map′ (cong (+_)) +-injective (m ℕ.≟ n) ++ m ≟ + n = map′ (cong (+_)) +-injective (m ℕ.≟ n) + m ≟ -[1+ n ] = no λ() -[1+ m ] ≟ + n = no λ() --[1+ m ] ≟ -[1+ n ] = Dec.map′ (cong -[1+_]) -[1+-injective (m ℕ.≟ n) +-[1+ m ] ≟ -[1+ n ] = map′ (cong -[1+_]) -[1+-injective (m ℕ.≟ n) ≡-setoid : Setoid 0ℓ 0ℓ ≡-setoid = setoid ℤ @@ -111,10 +110,10 @@ drop‿-≤- (-≤- n≤m) = n≤m infix 4 _≤?_ _≤?_ : Decidable _≤_ --[1+ m ] ≤? -[1+ n ] = Dec.map′ -≤- drop‿-≤- (n ℕ.≤? m) +-[1+ m ] ≤? -[1+ n ] = map′ -≤- drop‿-≤- (n ℕ.≤? m) -[1+ m ] ≤? + n = yes -≤+ + m ≤? -[1+ n ] = no λ () -+ m ≤? + n = Dec.map′ +≤+ drop‿+≤+ (m ℕ.≤? n) ++ m ≤? + n = map′ +≤+ drop‿+≤+ (m ℕ.≤? n) ≤-irrelevant : Irrelevant _≤_ ≤-irrelevant -≤+ -≤+ = refl @@ -302,10 +301,10 @@ drop‿-<- (-<- n Date: Sun, 13 Aug 2023 23:17:20 +0100 Subject: [PATCH 10/57] simplified imports for `Data.List.*\' --- src/Data/List/Fresh/Relation/Unary/All.agda | 4 ++-- src/Data/List/Fresh/Relation/Unary/Any.agda | 2 +- .../List/Membership/Propositional/Properties.agda | 12 +++++------- src/Data/List/Membership/Setoid/Properties.agda | 5 ++--- src/Data/List/NonEmpty/Base.agda | 2 +- src/Data/List/Properties.agda | 7 ++++--- 6 files changed, 15 insertions(+), 17 deletions(-) diff --git a/src/Data/List/Fresh/Relation/Unary/All.agda b/src/Data/List/Fresh/Relation/Unary/All.agda index 2f560e82c2..8b71a84fa4 100644 --- a/src/Data/List/Fresh/Relation/Unary/All.agda +++ b/src/Data/List/Fresh/Relation/Unary/All.agda @@ -11,7 +11,7 @@ module Data.List.Fresh.Relation.Unary.All where open import Level using (Level; _⊔_; Lift) open import Data.Product.Base using (_×_; _,_; proj₁; uncurry) open import Data.Sum.Base as Sum using (inj₁; inj₂) -open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_) +open import Relation.Nullary.Decidable.Core using (Dec; yes; no; map′; _×-dec_) open import Relation.Unary as U open import Relation.Binary.Core using (Rel) @@ -65,7 +65,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) = map′ (uncurry _∷_) uncons (P? x ×-dec 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 dbb9dd0dec..7a03010fae 100644 --- a/src/Data/List/Fresh/Relation/Unary/Any.agda +++ b/src/Data/List/Fresh/Relation/Unary/Any.agda @@ -13,7 +13,7 @@ open import Data.Empty open import Data.Product.Base using (∃; _,_; -,_) open import Data.Sum.Base using (_⊎_; [_,_]′; inj₁; inj₂) open import Function.Bundles using (_⇔_; mk⇔) -open import Relation.Nullary.Negation using (¬_) +open import Relation.Nullary.Negation.Core using (¬_) open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎-dec_) open import Relation.Unary as U open import Relation.Binary.Core using (Rel) diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda index dfef9fa160..149ce29c57 100644 --- a/src/Data/List/Membership/Propositional/Properties.agda +++ b/src/Data/List/Membership/Propositional/Properties.agda @@ -40,11 +40,9 @@ open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl; sym; trans; cong; subst; →-to-⟶; _≗_) import Relation.Binary.Properties.DecTotalOrder as DTOProperties open import Relation.Unary using (_⟨×⟩_; Decidable) -import Relation.Nullary.Reflects as Reflects +open import Relation.Nullary.Decidable.Core using (Dec; does; yes; no; ¬¬-excluded-middle) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Nullary.Reflects using (invert) -open import Relation.Nullary using (¬_; Dec; does; yes; no; _because_) -open import Relation.Nullary.Negation using (contradiction) -open import Relation.Nullary.Decidable using (¬¬-excluded-middle) private open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ}) @@ -373,13 +371,13 @@ finite inj (x ∷ xs) fᵢ∈x∷xs = ¬¬-excluded-middle helper lemma i≤j i≰1+j refl = i≰1+j (m≤n⇒m≤1+n i≤j) f′ⱼ∈xs : ∀ j → f′ j ∈ xs - f′ⱼ∈xs j with i ≤ᵇ j | Reflects.invert (≤ᵇ-reflects-≤ i j) + f′ⱼ∈xs j with i ≤ᵇ j | invert (≤ᵇ-reflects-≤ i j) ... | true | p = ∈-if-not-i (<⇒≢ (s≤s p)) ... | false | p = ∈-if-not-i (<⇒≢ (≰⇒> p) ∘ sym) f′-injective′ : Injective {B = P.setoid _} (→-to-⟶ f′) - f′-injective′ {j} {k} eq with i ≤ᵇ j | Reflects.invert (≤ᵇ-reflects-≤ i j) - | i ≤ᵇ k | Reflects.invert (≤ᵇ-reflects-≤ i k) + f′-injective′ {j} {k} eq with i ≤ᵇ j | invert (≤ᵇ-reflects-≤ i j) + | i ≤ᵇ k | invert (≤ᵇ-reflects-≤ i k) ... | true | p | true | q = P.cong pred (f-inj eq) ... | true | p | false | q = contradiction (f-inj eq) (lemma p q) ... | false | p | true | q = contradiction (f-inj eq) (lemma q p ∘ sym) diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda index 2fee07309f..76c7f40026 100644 --- a/src/Data/List/Membership/Setoid/Properties.agda +++ b/src/Data/List/Membership/Setoid/Properties.agda @@ -29,10 +29,9 @@ open import Level using (Level) open import Relation.Binary as B hiding (Decidable) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) open import Relation.Unary as U using (Decidable; Pred) -open import Relation.Nullary using (¬_; does; _because_; yes; no) +open import Relation.Nullary.Decidable.Core using (does; _because_; ¬?) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Nullary.Reflects using (invert) -open import Relation.Nullary.Negation using (contradiction) -open import Relation.Nullary.Decidable using (¬?) open Setoid using (Carrier) private diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda index 320cacd4b6..554a02391e 100644 --- a/src/Data/List/NonEmpty/Base.agda +++ b/src/Data/List/NonEmpty/Base.agda @@ -23,7 +23,7 @@ open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl) open import Relation.Unary using (Pred; Decidable; U; ∅) open import Relation.Unary.Properties using (U?; ∅?) -open import Relation.Nullary.Decidable using (does) +open import Relation.Nullary.Decidable.Core using (does) private variable diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index dd4326a749..f68df006d9 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -38,9 +38,10 @@ open import Relation.Binary.Definitions as B using (DecidableEquality) import Relation.Binary.Reasoning.Setoid as EqR open import Relation.Binary.PropositionalEquality as P hiding ([_]) open import Relation.Binary.Core using (Rel) +open import Relation.Nullary.Decidable.Core + using (Dec; does; _because_; yes; no; map′; ¬?; _×-dec_) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Nullary.Reflects using (invert) -open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no; contradiction) -open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋; ¬?; _×-dec_) open import Relation.Unary using (Pred; Decidable; ∁) open import Relation.Unary.Properties using (∁?) @@ -71,7 +72,7 @@ module _ {x y : A} {xs ys : List A} where ∷-injectiveʳ refl = refl ∷-dec : Dec (x ≡ y) → Dec (xs ≡ ys) → Dec (x List.∷ xs ≡ y ∷ ys) - ∷-dec x≟y xs≟ys = Decidable.map′ (uncurry (cong₂ _∷_)) ∷-injective (x≟y ×-dec xs≟ys) + ∷-dec x≟y xs≟ys = map′ (uncurry (cong₂ _∷_)) ∷-injective (x≟y ×-dec xs≟ys) ≡-dec : DecidableEquality A → DecidableEquality (List A) ≡-dec _≟_ [] [] = yes refl From 9729f53150cf7aad9a334f27ebcf1d618f8e9987 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 06:46:34 +0100 Subject: [PATCH 11/57] further simplified imports for `Data.List.*\'; plus some previously uncommitted tweaks --- README/Design/Decidability.agda | 3 +-- src/Data/Integer/Properties.agda | 2 +- src/Data/List/Membership/DecSetoid.agda | 2 +- .../Binary/Infix/Heterogeneous/Properties.agda | 4 ++-- .../Binary/Permutation/Setoid/Properties.agda | 4 ++-- src/Data/List/Relation/Binary/Pointwise.agda | 1 - .../List/Relation/Binary/Pointwise/Properties.agda | 5 ++--- .../Binary/Prefix/Heterogeneous/Properties.agda | 6 +++--- .../Binary/Sublist/Heterogeneous/Properties.agda | 14 +++++++------- .../Relation/Binary/Sublist/Setoid/Properties.agda | 4 ++-- .../Binary/Suffix/Heterogeneous/Properties.agda | 7 +++---- .../Ternary/Interleaving/Setoid/Properties.agda | 3 +-- src/Data/List/Relation/Unary/All.agda | 5 ++--- src/Data/List/Relation/Unary/AllPairs.agda | 4 ++-- .../List/Relation/Unary/AllPairs/Properties.agda | 2 +- src/Data/List/Relation/Unary/Any.agda | 7 +++---- src/Data/List/Relation/Unary/Any/Properties.agda | 13 ++++++------- src/Data/List/Relation/Unary/Grouped.agda | 4 ++-- src/Data/List/Relation/Unary/Linked.agda | 2 +- .../List/Relation/Unary/Linked/Properties.agda | 2 +- .../Unary/Sorted/TotalOrder/Properties.agda | 2 +- src/Data/List/Relation/Unary/Unique/DecSetoid.agda | 2 +- .../Unary/Unique/DecSetoid/Properties.agda | 2 +- src/Data/List/Sort/MergeSort.agda | 4 ++-- 24 files changed, 48 insertions(+), 56 deletions(-) diff --git a/README/Design/Decidability.agda b/README/Design/Decidability.agda index 1e0e3f50d5..c02eadad53 100644 --- a/README/Design/Decidability.agda +++ b/README/Design/Decidability.agda @@ -50,8 +50,7 @@ open import Relation.Nullary.Decidable -- proof : Reflects P does ex₃ : (b : Bool) → Dec (T b) -does (ex₃ b) = b -proof (ex₃ b) = ex₂ b +ex₃ = bool⁺ -- We also have pattern synonyms `yes` and `no`, allowing both fields to be -- given at once. diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 7a5a54aedd..d7f06ed066 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -30,8 +30,8 @@ open import Level using (0ℓ) open import Relation.Binary open import Relation.Binary.PropositionalEquality open import Relation.Nullary.Decidable.Core using (yes; no; map′) -open import Relation.Nullary.Reflects using (invert) open import Relation.Nullary.Negation.Core using (¬_; contradiction) +open import Relation.Nullary.Reflects using (invert) open import Algebra.Definitions {A = ℤ} _≡_ open import Algebra.Consequences.Propositional diff --git a/src/Data/List/Membership/DecSetoid.agda b/src/Data/List/Membership/DecSetoid.agda index 8f34aab9f6..6299c9dd2b 100644 --- a/src/Data/List/Membership/DecSetoid.agda +++ b/src/Data/List/Membership/DecSetoid.agda @@ -8,7 +8,7 @@ open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.Bundles using (DecSetoid) -open import Relation.Nullary.Decidable using (¬?) +open import Relation.Nullary.Decidable.Core using (¬?) module Data.List.Membership.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where diff --git a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda index 9af0162ded..0a9c585663 100644 --- a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda @@ -17,8 +17,8 @@ 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.Negation using (¬_; contradiction) +open import Relation.Nullary.Decidable.Core using (yes; no; does; map′; _⊎-dec_) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Unary as U using (Pred) open import Relation.Binary.Core using (REL; _⇒_) open import Relation.Binary.Definitions using (Decidable; Trans; Antisym) diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda index 57233a7b2a..1d4ce4bb35 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda @@ -41,8 +41,8 @@ open import Relation.Unary using (Pred; Decidable) open import Relation.Binary.Properties.Setoid S using (≉-resp₂) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_) -open import Relation.Nullary.Decidable using (yes; no; does) -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Decidable.Core using (yes; no; does) +open import Relation.Nullary.Negation.Core using (contradiction) private variable diff --git a/src/Data/List/Relation/Binary/Pointwise.agda b/src/Data/List/Relation/Binary/Pointwise.agda index 2728418ddc..a69375d0bb 100644 --- a/src/Data/List/Relation/Binary/Pointwise.agda +++ b/src/Data/List/Relation/Binary/Pointwise.agda @@ -23,7 +23,6 @@ open import Data.Nat.Base using (ℕ; zero; suc) open import Data.Nat.Properties open import Level open import Relation.Nullary hiding (Irrelevant) -import Relation.Nullary.Decidable as Dec using (map′) open import Relation.Unary as U using (Pred) open import Relation.Binary.Core renaming (Rel to Rel₂) open import Relation.Binary.Definitions using (_Respects_; _Respects₂_) diff --git a/src/Data/List/Relation/Binary/Pointwise/Properties.agda b/src/Data/List/Relation/Binary/Pointwise/Properties.agda index 7dfba09296..5b45e9ab54 100644 --- a/src/Data/List/Relation/Binary/Pointwise/Properties.agda +++ b/src/Data/List/Relation/Binary/Pointwise/Properties.agda @@ -14,8 +14,7 @@ open import Level open import Relation.Binary.Core using (REL; _⇒_) open import Relation.Binary.Definitions import Relation.Binary.PropositionalEquality.Core as P -open import Relation.Nullary using (yes; no; _×-dec_) -import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Decidable.Core using (yes; no; map′; _×-dec_) open import Data.List.Relation.Binary.Pointwise.Base @@ -68,7 +67,7 @@ decidable : Decidable R → Decidable (Pointwise R) decidable _ [] [] = yes [] decidable _ [] (y ∷ ys) = no λ() decidable _ (x ∷ xs) [] = no λ() -decidable R? (x ∷ xs) (y ∷ ys) = Dec.map′ (uncurry _∷_) uncons +decidable R? (x ∷ xs) (y ∷ ys) = map′ (uncurry _∷_) uncons (R? x y ×-dec decidable R? xs ys) irrelevant : Irrelevant R → Irrelevant (Pointwise R) diff --git a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda index 5706dbc36e..0c40ce5a7b 100644 --- a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda @@ -22,8 +22,8 @@ open import Data.Nat.Properties using (suc-injective) open import Data.Product.Base as Prod using (_×_; _,_; proj₁; proj₂; uncurry) open import Function.Base -open import Relation.Nullary.Negation using (¬_) -open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no; _because_) +open import Relation.Nullary.Negation.Core using (¬_) +open import Relation.Nullary.Decidable.Core using (_×-dec_; yes; no; _because_; map′) open import Relation.Unary as U using (Pred) open import Relation.Binary open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; _≢_) @@ -216,5 +216,5 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where prefix? : Decidable R → Decidable (Prefix R) prefix? R? [] bs = yes [] prefix? R? (a ∷ as) [] = no (λ ()) - prefix? R? (a ∷ as) (b ∷ bs) = Dec.map′ (uncurry _∷_) uncons + prefix? R? (a ∷ as) (b ∷ bs) = map′ (uncurry _∷_) uncons $ R? a b ×-dec prefix? R? as bs diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda index 46d5d7d2cc..4989280f45 100644 --- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda @@ -29,9 +29,9 @@ open import Data.Product.Base using (∃₂; _×_; _,_; <_,_>; proj₂; uncurry) open import Function.Base open import Function.Bundles using (_⤖_; _⇔_ ; mk⤖; mk⇔) open import Function.Consequences.Propositional using (strictlySurjective⇒surjective) +open import Relation.Nullary.Decidable.Core using (Dec; does; _because_; yes; no; map′; ¬?) +open import Relation.Nullary.Negation.Core using (¬_) open import Relation.Nullary.Reflects using (invert) -open import Relation.Nullary using (Dec; does; _because_; yes; no; ¬_) -open import Relation.Nullary.Decidable as Dec using (¬?) open import Relation.Unary as U using (Pred) open import Relation.Binary hiding (_⇔_) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) @@ -412,9 +412,9 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} (R? : Decidable R) wher sublist? (x ∷ xs) [] = no λ () sublist? (x ∷ xs) (y ∷ ys) with R? x y ... | true because [r] = - Dec.map (∷⁻¹ (invert [r])) (sublist? xs ys) + map′ ((invert [r]) ∷_) ∷⁻ (sublist? xs ys) ... | false because [¬r] = - Dec.map (∷ʳ⁻¹ (invert [¬r])) (sublist? (x ∷ xs) ys) + map′ (_ ∷ʳ_) (∷ʳ⁻ (invert [¬r])) (sublist? (x ∷ xs) ys) module _ {a e r} {A : Set a} {E : Rel A e} {R : Rel A r} where @@ -491,12 +491,12 @@ module Disjointness {a b r} {A : Set a} {B : Set b} {R : REL A B r} where ⊆-disjoint? (x≈z ∷ τ₁) (y≈z ∷ τ₂) = no λ() -- Present in either sublist: ok. ⊆-disjoint? (y ∷ʳ τ₁) (x≈y ∷ τ₂) = - Dec.map′ (x≈y ∷ᵣ_) (λ{ (_ ∷ᵣ d) → d }) (⊆-disjoint? τ₁ τ₂) + map′ (x≈y ∷ᵣ_) (λ{ (_ ∷ᵣ d) → d }) (⊆-disjoint? τ₁ τ₂) ⊆-disjoint? (x≈y ∷ τ₁) (y ∷ʳ τ₂) = - Dec.map′ (x≈y ∷ₗ_) (λ{ (_ ∷ₗ d) → d }) (⊆-disjoint? τ₁ τ₂) + map′ (x≈y ∷ₗ_) (λ{ (_ ∷ₗ d) → d }) (⊆-disjoint? τ₁ τ₂) -- Present in neither sublist: ok. ⊆-disjoint? (y ∷ʳ τ₁) (.y ∷ʳ τ₂) = - Dec.map′ (y ∷ₙ_) (λ{ (_ ∷ₙ d) → d }) (⊆-disjoint? τ₁ τ₂) + map′ (y ∷ₙ_) (λ{ (_ ∷ₙ d) → d }) (⊆-disjoint? τ₁ τ₂) -- Disjoint is proof-irrelevant diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda index 19fe765456..412f3efd97 100644 --- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda @@ -25,8 +25,8 @@ open import Relation.Binary.Definitions using () renaming (Decidable to Decidabl open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong) open import Relation.Binary.Structures using (IsDecTotalOrder) open import Relation.Unary using (Pred; Decidable; Irrelevant) -open import Relation.Nullary.Negation using (¬_) -open import Relation.Nullary.Decidable using (¬?; yes; no) +open import Relation.Nullary.Negation.Core using (¬_) +open import Relation.Nullary.Decidable.Core using (¬?; yes; no) import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality import Data.List.Relation.Binary.Sublist.Setoid as SetoidSublist diff --git a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda index 05b7725d31..e3e1b2771c 100644 --- a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda @@ -20,10 +20,9 @@ open import Data.List.Relation.Binary.Prefix.Heterogeneous as Prefix open import Data.Nat.Base open import Data.Nat.Properties open import Function.Base using (_$_; flip) -open import Relation.Nullary using (Dec; does; ¬_) -import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Decidable.Core using (does; map′) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Unary as U using (Pred) -open import Relation.Nullary.Negation using (contradiction) open import Relation.Binary as B using (REL; Rel; Trans; Antisym; Irrelevant; _⇒_) open import Relation.Binary.PropositionalEquality.Core as P @@ -207,5 +206,5 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where -- Decidability suffix? : B.Decidable R → B.Decidable (Suffix R) - suffix? R? as bs = Dec.map′ fromPrefix-rev toPrefix-rev + suffix? R? as bs = map′ fromPrefix-rev toPrefix-rev $ Prefixₚ.prefix? R? (reverse as) (reverse bs) diff --git a/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda b/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda index 936bca38b4..3805ec26e1 100644 --- a/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda +++ b/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda @@ -14,8 +14,7 @@ module Data.List.Relation.Ternary.Interleaving.Setoid.Properties open import Data.List.Base using (List; []; _∷_; filter; _++_) open import Data.Bool.Base using (true; false) open import Relation.Unary using (Decidable) -open import Relation.Nullary.Decidable using (does) -open import Relation.Nullary.Decidable using (¬?) +open import Relation.Nullary.Decidable.Core using (does; ¬?) open import Function.Base using (_∘_) open import Data.List.Relation.Binary.Equality.Setoid S using (≋-refl) diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda index 00d8e6f7b7..27b4a94b2c 100644 --- a/src/Data/List/Relation/Unary/All.agda +++ b/src/Data/List/Relation/Unary/All.agda @@ -20,8 +20,7 @@ open import Data.Product.Base as Prod open import Data.Sum.Base as Sum using (inj₁; inj₂) open import Function.Base using (_∘_; _∘′_; id; const) open import Level using (Level; _⊔_) -open import Relation.Nullary hiding (Irrelevant) -import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Decidable.Core using (yes; map′; _×-dec_) open import Relation.Unary hiding (_∈_) open import Relation.Binary using (Setoid; _Respects_) open import Relation.Binary.PropositionalEquality.Core as P @@ -205,7 +204,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) = map′ (uncurry _∷_) uncons (p x ×-dec 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 49bfac6ae0..50fb6fc7f6 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 as B using (Rel; _⇒_) open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_) open import Relation.Binary.PropositionalEquality 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.Core using (_×-dec_; yes; no; map′) ------------------------------------------------------------------------ -- 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) + map′ (uncurry _∷_) uncons (All.all? (R? x) xs ×-dec allPairs? R? xs) irrelevant : B.Irrelevant R → U.Irrelevant (AllPairs R) irrelevant irr [] [] = refl diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda index c116fcb00f..581150a4eb 100644 --- a/src/Data/List/Relation/Unary/AllPairs/Properties.agda +++ b/src/Data/List/Relation/Unary/AllPairs/Properties.agda @@ -23,7 +23,7 @@ open import Relation.Binary.Core using (Rel) open import Relation.Binary.Bundles using (DecSetoid) open import Relation.Binary.PropositionalEquality.Core using (_≢_) open import Relation.Unary using (Pred; Decidable) -open import Relation.Nullary.Decidable using (does) +open import Relation.Nullary.Decidable.Core using (does) private variable diff --git a/src/Data/List/Relation/Unary/Any.agda b/src/Data/List/Relation/Unary/Any.agda index eb010e2a39..a45a69ac72 100644 --- a/src/Data/List/Relation/Unary/Any.agda +++ b/src/Data/List/Relation/Unary/Any.agda @@ -14,9 +14,8 @@ open import Data.List.Base as List using (List; []; [_]; _∷_) open import Data.Product.Base as Prod using (∃; _,_) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂) open import Level using (Level; _⊔_) -open import Relation.Nullary using (¬_; yes; no; _⊎-dec_) -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Decidable.Core using (yes; no; map′; _⊎-dec_) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Unary hiding (_∈_) private @@ -90,7 +89,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) = map′ fromSum toSum (P? x ⊎-dec any? P? xs) satisfiable : Satisfiable P → Satisfiable (Any P) satisfiable (x , Px) = [ x ] , here Px diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda index 8f3bcd640c..e91df749a6 100644 --- a/src/Data/List/Relation/Unary/Any/Properties.agda +++ b/src/Data/List/Relation/Unary/Any/Properties.agda @@ -45,9 +45,8 @@ open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl) open import Relation.Unary as U using (Pred; _⟨×⟩_; _⟨→⟩_) renaming (_⊆_ to _⋐_) -open import Relation.Nullary using (¬_; _because_; does; ofʸ; ofⁿ; yes; no) -open import Relation.Nullary.Decidable using (¬?; decidable-stable) -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Decidable.Core using (does; yes; no; ¬?; decidable-stable) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) private open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ}) @@ -527,8 +526,8 @@ module _ (Q? : U.Decidable Q) where filter⁺ : (p : Any P xs) → Any P (filter Q? xs) ⊎ ¬ Q (Any.lookup p) filter⁺ {xs = x ∷ _} (here px) with Q? x - ... | true because _ = inj₁ (here px) - ... | false because ofⁿ ¬Qx = inj₂ ¬Qx + ... | yes _ = inj₁ (here px) + ... | no ¬Qx = inj₂ ¬Qx filter⁺ {xs = x ∷ _} (there p) with does (Q? x) ... | true = Sum.map₁ there (filter⁺ p) ... | false = filter⁺ p @@ -548,8 +547,8 @@ module _ {R : A → A → Set r} (R? : B.Decidable R) where derun⁺-aux : ∀ x xs → P Respects R → P x → Any P (derun R? (x ∷ xs)) derun⁺-aux x [] resp Px = here Px derun⁺-aux x (y ∷ xs) resp Px with R? x y - ... | true because ofʸ Rxy = derun⁺-aux y xs resp (resp Rxy Px) - ... | false because _ = here Px + ... | yes Rxy = derun⁺-aux y xs resp (resp Rxy Px) + ... | no _ = here Px derun⁺ : P Respects R → Any P xs → Any P (derun R? xs) derun⁺ {xs = x ∷ xs} resp (here px) = derun⁺-aux x xs resp px diff --git a/src/Data/List/Relation/Unary/Grouped.agda b/src/Data/List/Relation/Unary/Grouped.agda index 87b11cabc3..a28c37d46e 100644 --- a/src/Data/List/Relation/Unary/Grouped.agda +++ b/src/Data/List/Relation/Unary/Grouped.agda @@ -15,7 +15,7 @@ open import Data.Product.Base using (_×_; _,_) open import Relation.Binary as B using (REL; Rel) 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.Core using (yes; map′; ¬?; _⊎-dec_; _×-dec_) open import Level using (Level; _⊔_) private @@ -44,7 +44,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))) + map′ from to ((x ≟ y ⊎-dec all? (λ z → ¬? (x ≟ z)) (y ∷ xs)) ×-dec (grouped? _≟_ (y ∷ xs))) where from : ((x ≈ y) ⊎ All (λ z → ¬ (x ≈ z)) (y ∷ xs)) × Grouped _≈_ (y ∷ xs) → Grouped _≈_ (x ∷ y ∷ xs) from (inj₁ x≈y , grouped[y∷xs]) = x≈y ∷≈ grouped[y∷xs] diff --git a/src/Data/List/Relation/Unary/Linked.agda b/src/Data/List/Relation/Unary/Linked.agda index 38fcdd1507..ebf399716d 100644 --- a/src/Data/List/Relation/Unary/Linked.agda +++ b/src/Data/List/Relation/Unary/Linked.agda @@ -21,7 +21,7 @@ open import Relation.Binary.Core using (Rel; _⇒_) open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_) open import Relation.Binary.PropositionalEquality open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_) -open import Relation.Nullary.Decidable using (yes; no; map′; _×-dec_) +open import Relation.Nullary.Decidable.Core using (yes; no; map′; _×-dec_) private variable diff --git a/src/Data/List/Relation/Unary/Linked/Properties.agda b/src/Data/List/Relation/Unary/Linked/Properties.agda index d969986a55..288cfe28f1 100644 --- a/src/Data/List/Relation/Unary/Linked/Properties.agda +++ b/src/Data/List/Relation/Unary/Linked/Properties.agda @@ -25,7 +25,7 @@ open import Function.Base using (_∘_; flip; _on_) open import Relation.Binary using (Rel; Transitive; DecSetoid) open import Relation.Binary.PropositionalEquality.Core using (_≢_) open import Relation.Unary using (Pred; Decidable) -open import Relation.Nullary.Decidable using (yes; no; does) +open import Relation.Nullary.Decidable.Core using (yes; no; does) private variable diff --git a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda index 89582d2f88..31fcc92dc7 100644 --- a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda +++ b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda @@ -26,7 +26,7 @@ open import Level using (Level) open import Relation.Binary hiding (Decidable) import Relation.Binary.Properties.TotalOrder as TotalOrderProperties open import Relation.Unary using (Pred; Decidable) -open import Relation.Nullary.Decidable using (yes; no) +open import Relation.Nullary.Decidable.Core using (yes; no) private variable diff --git a/src/Data/List/Relation/Unary/Unique/DecSetoid.agda b/src/Data/List/Relation/Unary/Unique/DecSetoid.agda index 4b7133c8f1..4035247b57 100644 --- a/src/Data/List/Relation/Unary/Unique/DecSetoid.agda +++ b/src/Data/List/Relation/Unary/Unique/DecSetoid.agda @@ -9,7 +9,7 @@ open import Relation.Binary using (DecSetoid) import Data.List.Relation.Unary.AllPairs as AllPairs open import Relation.Unary using (Decidable) -open import Relation.Nullary.Decidable using (¬?) +open import Relation.Nullary.Decidable.Core using (¬?) module Data.List.Relation.Unary.Unique.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where diff --git a/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda b/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda index 2eda2ded13..7a6b0b4205 100644 --- a/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda +++ b/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda @@ -12,7 +12,7 @@ open import Data.List.Relation.Unary.All.Properties using (all-filter) open import Data.List.Relation.Unary.Unique.Setoid.Properties open import Level open import Relation.Binary using (DecSetoid) -open import Relation.Nullary.Decidable using (¬?) +open import Relation.Nullary.Decidable.Core using (¬?) module Data.List.Relation.Unary.Unique.DecSetoid.Properties where diff --git a/src/Data/List/Sort/MergeSort.agda b/src/Data/List/Sort/MergeSort.agda index 9648718d0d..77510731a4 100644 --- a/src/Data/List/Sort/MergeSort.agda +++ b/src/Data/List/Sort/MergeSort.agda @@ -20,14 +20,14 @@ import Data.List.Relation.Unary.All.Properties as All open import Data.List.Relation.Binary.Permutation.Propositional import Data.List.Relation.Binary.Permutation.Propositional.Properties as Perm open import Data.Maybe.Base using (just) -open import Relation.Nullary.Decidable using (does) open import Data.Nat using (_<_; _>_; z Date: Mon, 14 Aug 2023 06:59:59 +0100 Subject: [PATCH 12/57] simplified imports for `Data.Maybe.*\' --- src/Data/Maybe/Base.agda | 7 +++---- src/Data/Maybe/Properties.agda | 3 +-- src/Data/Maybe/Relation/Binary/Connected.agda | 5 ++--- src/Data/Maybe/Relation/Binary/Pointwise.agda | 5 ++--- src/Data/Maybe/Relation/Unary/All.agda | 5 ++--- src/Data/Maybe/Relation/Unary/Any.agda | 5 ++--- 6 files changed, 12 insertions(+), 18 deletions(-) diff --git a/src/Data/Maybe/Base.agda b/src/Data/Maybe/Base.agda index b0ae001f46..08f843867e 100644 --- a/src/Data/Maybe/Base.agda +++ b/src/Data/Maybe/Base.agda @@ -16,8 +16,7 @@ open import Data.Unit.Base using (⊤) open import Data.These.Base using (These; this; that; these) open import Data.Product.Base as Prod using (_×_; _,_) open import Function.Base -open import Relation.Nullary.Reflects -open import Relation.Nullary.Decidable.Core +open import Relation.Nullary.Decidable.Core using (Dec; yes; no) private variable @@ -47,8 +46,8 @@ is-nothing : Maybe A → Bool is-nothing = not ∘ is-just decToMaybe : Dec A → Maybe A -decToMaybe ( true because [a]) = just (invert [a]) -decToMaybe (false because _ ) = nothing +decToMaybe (yes a) = just a +decToMaybe (no _) = nothing -- A dependent eliminator. diff --git a/src/Data/Maybe/Properties.agda b/src/Data/Maybe/Properties.agda index 4940da433f..37eef3c0c0 100644 --- a/src/Data/Maybe/Properties.agda +++ b/src/Data/Maybe/Properties.agda @@ -19,8 +19,7 @@ open import Function.Definitions using (Injective) open import Level using (Level) open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.PropositionalEquality -open import Relation.Nullary.Decidable using (yes; no) -open import Relation.Nullary.Decidable using (map′) +open import Relation.Nullary.Decidable.Core using (yes; no; map′) private variable diff --git a/src/Data/Maybe/Relation/Binary/Connected.agda b/src/Data/Maybe/Relation/Binary/Connected.agda index 5c509e50fd..a6f378441c 100644 --- a/src/Data/Maybe/Relation/Binary/Connected.agda +++ b/src/Data/Maybe/Relation/Binary/Connected.agda @@ -13,8 +13,7 @@ open import Data.Maybe.Base using (Maybe; just; nothing) open import Function.Bundles using (_⇔_; mk⇔) open import Relation.Binary hiding (_⇔_) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) -open import Relation.Nullary -import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Decidable.Core using (yes; map′) private variable @@ -60,7 +59,7 @@ sym R-sym just-nothing = nothing-just sym R-sym nothing = nothing connected? : Decidable R → Decidable (Connected R) -connected? R? (just x) (just y) = Dec.map just-equivalence (R? x y) +connected? R? (just x) (just y) = map′ just drop-just (R? x y) connected? R? (just x) nothing = yes just-nothing connected? R? nothing (just y) = yes nothing-just connected? R? nothing nothing = yes nothing diff --git a/src/Data/Maybe/Relation/Binary/Pointwise.agda b/src/Data/Maybe/Relation/Binary/Pointwise.agda index a9946a6ef3..bce1223aa4 100644 --- a/src/Data/Maybe/Relation/Binary/Pointwise.agda +++ b/src/Data/Maybe/Relation/Binary/Pointwise.agda @@ -14,8 +14,7 @@ open import Data.Maybe.Base using (Maybe; just; nothing) open import Function.Bundles using (_⇔_; mk⇔) open import Relation.Binary hiding (_⇔_) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) -open import Relation.Nullary -import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Decidable.Core using (yes; no; map′) ------------------------------------------------------------------------ -- Definition @@ -72,7 +71,7 @@ module _ {a b c r₁ r₂ r₃} {A : Set a} {B : Set b} {C : Set c} module _ {a r} {A : Set a} {R : Rel A r} where dec : Decidable R → Decidable (Pointwise R) - dec R-dec (just x) (just y) = Dec.map just-equivalence (R-dec x y) + dec R-dec (just x) (just y) = map′ just drop-just (R-dec x y) dec R-dec (just x) nothing = no (λ ()) dec R-dec nothing (just y) = no (λ ()) dec R-dec nothing nothing = yes nothing diff --git a/src/Data/Maybe/Relation/Unary/All.agda b/src/Data/Maybe/Relation/Unary/All.agda index c070bd279d..db305095c0 100644 --- a/src/Data/Maybe/Relation/Unary/All.agda +++ b/src/Data/Maybe/Relation/Unary/All.agda @@ -18,8 +18,7 @@ open import Function.Bundles using (_⇔_; mk⇔) open import Level open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; cong) open import Relation.Unary -open import Relation.Nullary hiding (Irrelevant) -import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Decidable.Core using (yes; map′) ------------------------------------------------------------------------ -- Definition @@ -106,7 +105,7 @@ module _ {a p} {A : Set a} {P : Pred A p} where dec : Decidable P → Decidable (All P) dec P-dec nothing = yes nothing - dec P-dec (just x) = Dec.map just-equivalence (P-dec x) + dec P-dec (just x) = map′ just drop-just (P-dec x) universal : Universal P → Universal (All P) universal P-universal (just x) = just (P-universal x) diff --git a/src/Data/Maybe/Relation/Unary/Any.agda b/src/Data/Maybe/Relation/Unary/Any.agda index 48cd402ce0..83979f309e 100644 --- a/src/Data/Maybe/Relation/Unary/Any.agda +++ b/src/Data/Maybe/Relation/Unary/Any.agda @@ -15,8 +15,7 @@ open import Function.Bundles using (_⇔_; mk⇔) open import Level open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; cong) open import Relation.Unary -open import Relation.Nullary hiding (Irrelevant) -import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Decidable.Core as Dec using (no; map′) ------------------------------------------------------------------------ -- Definition @@ -67,7 +66,7 @@ module _ {a p} {A : Set a} {P : Pred A p} where dec : Decidable P → Decidable (Any P) dec P-dec nothing = no λ () - dec P-dec (just x) = Dec.map just-equivalence (P-dec x) + dec P-dec (just x) = map′ just drop-just (P-dec x) irrelevant : Irrelevant P → Irrelevant (Any P) irrelevant P-irrelevant (just p) (just q) = cong just (P-irrelevant p q) From a2534c6557bebcd0584b43a84fd07ba2216d1a9e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 07:30:41 +0100 Subject: [PATCH 13/57] simplified imports for `Data.Nat.*\' --- src/Data/Nat/Binary/Properties.agda | 9 ++++----- src/Data/Nat/Combinatorics/Specification.agda | 4 ++-- src/Data/Nat/DivMod.agda | 3 +-- src/Data/Nat/DivMod/Core.agda | 4 ++-- src/Data/Nat/Divisibility.agda | 4 ++-- src/Data/Nat/GCD.agda | 9 ++++----- src/Data/Nat/LCM.agda | 2 +- src/Data/Nat/Primality.agda | 10 +++++----- src/Data/Nat/Properties.agda | 4 ++-- src/Data/Nat/Show.agda | 2 +- src/Data/Nat/Show/Properties.agda | 2 +- 11 files changed, 25 insertions(+), 28 deletions(-) diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index 43496f3139..600113ae59 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -33,9 +33,8 @@ open import Relation.Binary.Morphism import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphism open import Relation.Binary.PropositionalEquality import Relation.Binary.Reasoning.Base.Triple as InequalityReasoning -open import Relation.Nullary using (¬_; yes; no) -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Decidable.Core using (yes; no; map′) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Algebra.Definitions {A = ℕᵇ} _≡_ open import Algebra.Structures {A = ℕᵇ} _≡_ @@ -73,11 +72,11 @@ zero ≟ zero = yes refl zero ≟ 2[1+ _ ] = no λ() zero ≟ 1+[2 _ ] = no λ() 2[1+ _ ] ≟ zero = no λ() -2[1+ x ] ≟ 2[1+ y ] = Dec.map′ (cong 2[1+_]) 2[1+_]-injective (x ≟ y) +2[1+ x ] ≟ 2[1+ y ] = map′ (cong 2[1+_]) 2[1+_]-injective (x ≟ y) 2[1+ _ ] ≟ 1+[2 _ ] = no λ() 1+[2 _ ] ≟ zero = no λ() 1+[2 _ ] ≟ 2[1+ _ ] = no λ() -1+[2 x ] ≟ 1+[2 y ] = Dec.map′ (cong 1+[2_]) 1+[2_]-injective (x ≟ y) +1+[2 x ] ≟ 1+[2 y ] = map′ (cong 1+[2_]) 1+[2_]-injective (x ≟ y) ≡-isDecEquivalence : IsDecEquivalence {A = ℕᵇ} _≡_ ≡-isDecEquivalence = isDecEquivalence _≟_ diff --git a/src/Data/Nat/Combinatorics/Specification.agda b/src/Data/Nat/Combinatorics/Specification.agda index 0b263eed54..95a637037d 100644 --- a/src/Data/Nat/Combinatorics/Specification.agda +++ b/src/Data/Nat/Combinatorics/Specification.agda @@ -19,8 +19,8 @@ open import Data.Nat.Combinatorics.Base open import Data.Sum.Base using (inj₁; inj₂) open import Relation.Binary.PropositionalEquality using (_≡_; trans; _≢_) -open import Relation.Nullary.Decidable using (yes; no; does) -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Decidable.Core using (yes; no) +open import Relation.Nullary.Negation.Core using (contradiction) open import Relation.Binary.PropositionalEquality using (subst; refl; sym; cong; cong₂) diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda index c879cec098..ea43420f0f 100644 --- a/src/Data/Nat/DivMod.agda +++ b/src/Data/Nat/DivMod.agda @@ -19,8 +19,7 @@ open import Data.Nat.Induction open import Data.Nat.Properties open import Function.Base using (_$_) open import Relation.Binary.PropositionalEquality -open import Relation.Nullary.Decidable using (yes; no) -open import Relation.Nullary.Decidable using (False; toWitnessFalse) +open import Relation.Nullary.Decidable.Core using (yes; no) open ≤-Reasoning diff --git a/src/Data/Nat/DivMod/Core.agda b/src/Data/Nat/DivMod/Core.agda index 8ada6d77b2..cbe6ab2417 100644 --- a/src/Data/Nat/DivMod/Core.agda +++ b/src/Data/Nat/DivMod/Core.agda @@ -16,8 +16,8 @@ open import Data.Nat.Properties open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Data.Product.Base using (_×_; _,_) open import Relation.Binary.PropositionalEquality -open import Relation.Nullary.Decidable using (yes; no) -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Decidable.Core using (yes; no) +open import Relation.Nullary.Negation.Core using (contradiction) open ≤-Reasoning diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index 1b1321906d..3a6843f4c5 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -16,7 +16,7 @@ open import Data.Unit.Base using (tt) open import Function.Base using (_∘′_; _$_) open import Function.Bundles using (_⇔_; mk⇔) open import Level using (0ℓ) -open import Relation.Nullary.Decidable as Dec using (False; yes; no) +open import Relation.Nullary.Decidable.Core using (yes; no; map′) open import Relation.Nullary.Negation.Core using (contradiction) open import Relation.Binary import Relation.Binary.Reasoning.Preorder as PreorderReasoning @@ -83,7 +83,7 @@ infix 4 _∣?_ _∣?_ : Decidable _∣_ zero ∣? zero = yes (divides-refl 0) zero ∣? suc m = no ((λ()) ∘′ ∣-antisym (divides-refl 0)) -suc n ∣? m = Dec.map (m%n≡0⇔n∣m m (suc n)) (m % suc n ≟ 0) +n@(suc _) ∣? m = map′ (m%n≡0⇒n∣m m n) (n∣m⇒m%n≡0 m n) (m % n ≟ 0) ∣-isPreorder : IsPreorder _≡_ _∣_ ∣-isPreorder = record diff --git a/src/Data/Nat/GCD.agda b/src/Data/Nat/GCD.agda index f54b09e47f..b19ed96289 100644 --- a/src/Data/Nat/GCD.agda +++ b/src/Data/Nat/GCD.agda @@ -24,9 +24,8 @@ open import Induction.Lexicographic using (_⊗_; [_⊗_]) open import Relation.Binary open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; _≢_; subst; cong) -open import Relation.Nullary.Decidable using (Dec) -open import Relation.Nullary.Negation using (contradiction) -import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Decidable.Core using (Dec; map′) +open import Relation.Nullary.Negation.Core using (contradiction) open import Algebra.Definitions {A = ℕ} _≡_ as Algebra using (Associative; Commutative; LeftIdentity; RightIdentity; LeftZero; RightZero; Zero) @@ -280,8 +279,8 @@ mkGCD m n = gcd m n , gcd-GCD m n gcd? : (m n d : ℕ) → Dec (GCD m n d) gcd? m n d = - Dec.map′ (λ { P.refl → gcd-GCD m n }) (GCD.unique (gcd-GCD m n)) - (gcd m n ≟ d) + map′ (λ { P.refl → gcd-GCD m n }) (GCD.unique (gcd-GCD m n)) + (gcd m n ≟ d) GCD-* : ∀ {m n d c} .{{_ : NonZero c}} → GCD (m * c) (n * c) (d * c) → GCD m n d GCD-* {c = suc _} (GCD.is (dc∣nc , dc∣mc) dc-greatest) = diff --git a/src/Data/Nat/LCM.agda b/src/Data/Nat/LCM.agda index ccb1fbbf5b..51d45f1951 100644 --- a/src/Data/Nat/LCM.agda +++ b/src/Data/Nat/LCM.agda @@ -20,7 +20,7 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning) open import Relation.Binary -open import Relation.Nullary.Decidable using (False; fromWitnessFalse) + private -- instance diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 8e72b32be0..1473eb129c 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -16,9 +16,9 @@ open import Data.Nat.Properties open import Data.Product.Base using (∃; _×_; map₂; _,_) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Function.Base using (flip; _∘_; _∘′_) -open import Relation.Nullary.Decidable as Dec - using (yes; no; from-yes; ¬?; decidable-stable; _×-dec_; _→-dec_) -open import Relation.Nullary.Negation using (¬_; contradiction) +open import Relation.Nullary.Decidable + using (yes; no; from-yes; map′; ¬?; decidable-stable; _×-dec_; _→-dec_) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Unary using (Decidable) open import Relation.Binary.PropositionalEquality using (refl; cong) @@ -50,7 +50,7 @@ Prime n = ∀ {d} → 2 ≤ d → d < n → d ∤ n composite? : Decidable Composite composite? 0 = no λ() composite? 1 = no λ() -composite? n@(suc (suc _)) = Dec.map′ +composite? n@(suc (suc _)) = map′ (map₂ λ { (a , b , c) → (b , a , c)}) (map₂ λ { (a , b , c) → (b , a , c)}) (anyUpTo? (λ d → 2 ≤? d ×-dec d ∣? n) n) @@ -58,7 +58,7 @@ composite? n@(suc (suc _)) = Dec.map′ prime? : Decidable Prime prime? 0 = no λ() prime? 1 = no λ() -prime? n@(suc (suc _)) = Dec.map′ +prime? n@(suc (suc _)) = map′ (λ f {d} → flip (f {d})) (λ f {d} → flip (f {d})) (allUpTo? (λ d → 2 ≤? d →-dec ¬? (d ∣? n)) n) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 2b9a2a4819..3085a9baab 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -35,8 +35,8 @@ open import Relation.Binary open import Relation.Binary.Consequences using (flip-Connex) open import Relation.Binary.PropositionalEquality open import Relation.Nullary hiding (Irrelevant) -open import Relation.Nullary.Decidable using (True; via-injection; map′) -open import Relation.Nullary.Negation using (contradiction; contradiction₂) +open import Relation.Nullary.Decidable using (via-injection; map′) +open import Relation.Nullary.Negation.Core using (contradiction; contradiction₂) open import Relation.Nullary.Reflects using (fromEquivalence) open import Algebra.Definitions {A = ℕ} _≡_ diff --git a/src/Data/Nat/Show.agda b/src/Data/Nat/Show.agda index 23ab91b0fd..959a86386b 100644 --- a/src/Data/Nat/Show.agda +++ b/src/Data/Nat/Show.agda @@ -19,7 +19,7 @@ open import Data.Nat open import Data.Product.Base using (proj₁) open import Data.String.Base using (toList; fromList; String) open import Function.Base using (_∘′_; _∘_) -open import Relation.Nullary.Decidable using (True) +open import Relation.Nullary.Decidable.Core using (True) ------------------------------------------------------------------------ -- Read diff --git a/src/Data/Nat/Show/Properties.agda b/src/Data/Nat/Show/Properties.agda index 564264946c..38a68400c6 100644 --- a/src/Data/Nat/Show/Properties.agda +++ b/src/Data/Nat/Show/Properties.agda @@ -12,7 +12,7 @@ open import Function.Base using (_∘_) import Data.List.Properties as Listₚ open import Data.Nat.Base using (ℕ) open import Data.Nat.Properties using (_≤?_) -open import Relation.Nullary.Decidable using (True) +open import Relation.Nullary.Decidable.Core using (True) open import Relation.Binary.PropositionalEquality.Core using (_≡_) open import Data.Nat.Show using (charsInBase) From ab5c40d623031eea08532ea53c60662ecf12e807 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 07:45:27 +0100 Subject: [PATCH 14/57] simplified imports for `Data.Product.*\' --- src/Data/Product/Properties.agda | 4 ++-- src/Data/Product/Relation/Binary/Lex/Strict.agda | 2 +- .../Product/Relation/Binary/Pointwise/NonDependent.agda | 2 +- src/Data/Rational/Properties.agda | 9 ++++----- 4 files changed, 8 insertions(+), 9 deletions(-) diff --git a/src/Data/Product/Properties.agda b/src/Data/Product/Properties.agda index e741f8976a..ef1fbe754c 100644 --- a/src/Data/Product/Properties.agda +++ b/src/Data/Product/Properties.agda @@ -15,7 +15,7 @@ open import Function.Bundles using (_↔_; mk↔′) open import Level using (Level) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality -open import Relation.Nullary.Decidable as Dec using (Dec; yes; no) +open import Relation.Nullary.Decidable.Core using (Dec; yes; no; map′) private variable @@ -43,7 +43,7 @@ module _ {B : A → Set b} where DecidableEquality (Σ A B) ≡-dec dec₁ dec₂ (a , x) (b , y) with dec₁ a b ... | no [a≢b] = no ([a≢b] ∘ ,-injectiveˡ) - ... | yes refl = Dec.map′ (cong (a ,_)) (,-injectiveʳ-UIP (Decidable⇒UIP.≡-irrelevant dec₁)) (dec₂ x y) + ... | yes refl = map′ (cong (a ,_)) (,-injectiveʳ-UIP (Decidable⇒UIP.≡-irrelevant dec₁)) (dec₂ x y) ------------------------------------------------------------------------ -- Equality (non-dependent) diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda index d0a09fa4ac..54c42e3fa6 100644 --- a/src/Data/Product/Relation/Binary/Lex/Strict.agda +++ b/src/Data/Product/Relation/Binary/Lex/Strict.agda @@ -19,7 +19,7 @@ open import Data.Empty open import Function.Base open import Induction.WellFounded open import Level -open import Relation.Nullary.Decidable +open import Relation.Nullary.Decidable.Core using (_⊎-dec_; _×-dec_) open import Relation.Binary open import Relation.Binary.Consequences open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl) diff --git a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda index 16756bf375..31209bed84 100644 --- a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda +++ b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda @@ -25,7 +25,7 @@ open import Function.LeftInverse as LeftInv open import Function.Related open import Function.Surjection as Surj using (Surjection; _↠_; module Surjection) -open import Relation.Nullary.Decidable using (_×-dec_) +open import Relation.Nullary.Decidable.Core using (_×-dec_) open import Relation.Binary open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) import Relation.Binary.PropositionalEquality.Properties as P diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index 7c74cd2513..009d799369 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -53,9 +53,8 @@ open import Relation.Binary open import Relation.Binary.PropositionalEquality open import Relation.Binary.Morphism.Structures import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphisms -open import Relation.Nullary.Decidable as Dec - using (True; False; fromWitness; fromWitnessFalse; toWitnessFalse; yes; no; recompute; map′; _×-dec_) -open import Relation.Nullary.Negation using (¬_; contradiction; contraposition) +open import Relation.Nullary.Decidable.Core using (yes; no; map′; _×-dec_) +open import Relation.Nullary.Negation.Core using (¬_; contradiction; contraposition) open import Algebra.Definitions {A = ℚ} _≡_ open import Algebra.Structures {A = ℚ} _≡_ @@ -499,7 +498,7 @@ private infix 4 _≤?_ _≥?_ _≤?_ : Decidable _≤_ -p ≤? q = Dec.map′ *≤* drop-*≤* (↥ p ℤ.* ↧ q ℤ.≤? ↥ q ℤ.* ↧ p) +p ≤? q = map′ *≤* drop-*≤* (↥ p ℤ.* ↧ q ℤ.≤? ↥ q ℤ.* ↧ p) _≥?_ : Decidable _≥_ _≥?_ = flip _≤?_ @@ -646,7 +645,7 @@ toℚᵘ-isOrderMonomorphism-< = record infix 4 _?_ _?_ : Decidable _>_ _>?_ = flip _ Date: Mon, 14 Aug 2023 07:50:00 +0100 Subject: [PATCH 15/57] simplified imports for `Data.Record.*\' --- src/Data/Rational/Unnormalised/Properties.agda | 15 +++++++-------- src/Data/Record.agda | 3 +-- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 2945a8654a..8eb906faa7 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -31,9 +31,8 @@ open import Data.Sum.Base using (_⊎_; [_,_]′; inj₁; inj₂) import Data.Sign as Sign open import Function.Base using (_on_; _$_; _∘_; flip) open import Level using (0ℓ) -open import Relation.Nullary using (¬_; yes; no) -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Negation using (contradiction; contraposition) +open import Relation.Nullary.Decidable.Core using (yes; no; from-no; map′; decidable-stable) +open import Relation.Nullary.Negation.Core using (¬_; contradiction; contraposition) open import Relation.Binary import Relation.Binary.Consequences as BC open import Relation.Binary.PropositionalEquality @@ -98,10 +97,10 @@ drop-*≡* (*≡* eq) = eq infix 4 _≃?_ _≃?_ : Decidable _≃_ -p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* ↧ p) +p ≃? q = map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* ↧ p) 0≠1 : 0ℚᵘ ≠ 1ℚᵘ -0≠1 = Dec.from-no (0ℚᵘ ≃? 1ℚᵘ) +0≠1 = from-no (0ℚᵘ ≃? 1ℚᵘ) ≃-≠-irreflexive : Irreflexive _≃_ _≠_ ≃-≠-irreflexive x≃y x≠y = x≠y x≃y @@ -136,7 +135,7 @@ p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* } ≠-tight : Tight _≃_ _≠_ -proj₁ (≠-tight p q) ¬p≠q = Dec.decidable-stable (p ≃? q) ¬p≠q +proj₁ (≠-tight p q) ¬p≠q = decidable-stable (p ≃? q) ¬p≠q proj₂ (≠-tight p q) p≃q p≠q = p≠q p≃q ≃-setoid : Setoid 0ℓ 0ℓ @@ -247,7 +246,7 @@ drop-*≤* (*≤* pq≤qp) = pq≤qp infix 4 _≤?_ _≥?_ _≤?_ : Decidable _≤_ -p ≤? q = Dec.map′ *≤* drop-*≤* (↥ p ℤ.* ↧ q ℤ.≤? ↥ q ℤ.* ↧ p) +p ≤? q = map′ *≤* drop-*≤* (↥ p ℤ.* ↧ q ℤ.≤? ↥ q ℤ.* ↧ p) _≥?_ : Decidable _≥_ _≥?_ = flip _≤?_ @@ -450,7 +449,7 @@ drop-*<* (*<* pq?_ _?_ : Decidable _>_ _>?_ = flip _ Date: Mon, 14 Aug 2023 07:56:04 +0100 Subject: [PATCH 16/57] simplified imports for `Data.Sign.*\' --- src/Data/Sign/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Sign/Properties.agda b/src/Data/Sign/Properties.agda index 7ac07167e7..76afabd2de 100644 --- a/src/Data/Sign/Properties.agda +++ b/src/Data/Sign/Properties.agda @@ -18,7 +18,7 @@ open import Level using (0ℓ) open import Relation.Binary using (Decidable; DecidableEquality; Setoid; DecSetoid; IsDecEquivalence) open import Relation.Binary.PropositionalEquality -open import Relation.Nullary.Decidable using (yes; no) +open import Relation.Nullary.Decidable.Core using (yes; no) open import Algebra.Structures {A = Sign} _≡_ open import Algebra.Definitions {A = Sign} _≡_ From f6ff90205b3b7176978de590b533e59226440fd2 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 07:56:46 +0100 Subject: [PATCH 17/57] tweak use of `invert` --- src/Relation/Nullary/Decidable.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda index 5793725f0e..a91a02b80a 100644 --- a/src/Relation/Nullary/Decidable.agda +++ b/src/Relation/Nullary/Decidable.agda @@ -60,8 +60,8 @@ module _ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} -- A lemma relating True and Dec True-↔ : (dec : Dec P) → Irrelevant P → True dec ↔ P -True-↔ (true because [p]) irr = mk↔′ (λ _ → invert [p]) _ (irr (invert [p])) cong′ -True-↔ (false because ofⁿ ¬p) _ = mk↔′ (λ ()) (invert (ofⁿ ¬p)) (⊥-elim ∘ ¬p) λ () +True-↔ (yes p) irr = mk↔′ (λ _ → p) _ (irr p) cong′ +True-↔ (no ¬p) _ = mk↔′ (λ ()) ¬p (⊥-elim ∘ ¬p) λ () ------------------------------------------------------------------------ -- Result of decidability From fcd8cea8de8c03bd940caf9af64f6c0a9b4db2ae Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 08:00:43 +0100 Subject: [PATCH 18/57] simplified imports for `Data.String.*\' --- src/Data/String.agda | 2 +- src/Data/String/Properties.agda | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Data/String.agda b/src/Data/String.agda index 6a63342ccd..8081fab467 100644 --- a/src/Data/String.agda +++ b/src/Data/String.agda @@ -23,7 +23,7 @@ open import Data.Char.Base as Char using (Char) import Data.Char.Properties as Char using (_≟_) open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) -open import Relation.Nullary.Decidable using (does) +open import Relation.Nullary.Decidable.Core using (does) open import Relation.Unary using (Pred; Decidable) open import Data.List.Membership.DecPropositional Char._≟_ diff --git a/src/Data/String/Properties.agda b/src/Data/String/Properties.agda index beb0d869d8..1a2c7033af 100644 --- a/src/Data/String/Properties.agda +++ b/src/Data/String/Properties.agda @@ -15,8 +15,7 @@ import Data.List.Relation.Binary.Pointwise as Pointwise import Data.List.Relation.Binary.Lex.Strict as StrictLex open import Data.String.Base open import Function.Base -open import Relation.Nullary.Decidable using (yes; no) -open import Relation.Nullary.Decidable using (map′; isYes) +open import Relation.Nullary.Decidable.Core using (yes; no; map′; isYes) open import Relation.Binary open import Relation.Binary.PropositionalEquality.Core import Relation.Binary.Construct.On as On From 5e73cf9ffb00bdcab9f3d87c114a69a12cc5d932 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 08:03:32 +0100 Subject: [PATCH 19/57] simplified imports for `Data.Sum.*\' --- src/Data/Sum/Properties.agda | 3 +-- src/Data/Sum/Relation/Binary/LeftOrder.agda | 7 +++---- src/Data/Sum/Relation/Binary/Pointwise.agda | 7 +++---- 3 files changed, 7 insertions(+), 10 deletions(-) diff --git a/src/Data/Sum/Properties.agda b/src/Data/Sum/Properties.agda index 1ee329a2d5..d06a98330c 100644 --- a/src/Data/Sum/Properties.agda +++ b/src/Data/Sum/Properties.agda @@ -14,8 +14,7 @@ open import Function.Base using (_∋_; _∘_; id) open import Function.Bundles using (mk↔′; _↔_) open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.PropositionalEquality -open import Relation.Nullary.Decidable using (yes; no) -open import Relation.Nullary.Decidable using (map′) +open import Relation.Nullary.Decidable.Core using (yes; no; map′) private diff --git a/src/Data/Sum/Relation/Binary/LeftOrder.agda b/src/Data/Sum/Relation/Binary/LeftOrder.agda index 1ff3b18d05..8656a273f9 100644 --- a/src/Data/Sum/Relation/Binary/LeftOrder.agda +++ b/src/Data/Sum/Relation/Binary/LeftOrder.agda @@ -15,8 +15,7 @@ open import Data.Product.Base using (_,_) open import Data.Empty open import Function.Base using (_$_; _∘_) open import Level -open import Relation.Nullary -import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Decidable.Core using (yes; no; map′) open import Relation.Binary open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) @@ -73,10 +72,10 @@ module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂} ⊎-<-decidable : Decidable ∼₁ → Decidable ∼₂ → Decidable (∼₁ ⊎-< ∼₂) - ⊎-<-decidable dec₁ dec₂ (inj₁ x) (inj₁ y) = Dec.map′ ₁∼₁ drop-inj₁ (dec₁ x y) + ⊎-<-decidable dec₁ dec₂ (inj₁ x) (inj₁ y) = map′ ₁∼₁ drop-inj₁ (dec₁ x y) ⊎-<-decidable dec₁ dec₂ (inj₁ x) (inj₂ y) = yes ₁∼₂ ⊎-<-decidable dec₁ dec₂ (inj₂ x) (inj₁ y) = no λ() - ⊎-<-decidable dec₁ dec₂ (inj₂ x) (inj₂ y) = Dec.map′ ₂∼₂ drop-inj₂ (dec₂ x y) + ⊎-<-decidable dec₁ dec₂ (inj₂ x) (inj₂ y) = map′ ₂∼₂ drop-inj₂ (dec₂ x y) module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂} {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {≈₁ : Rel A₁ ℓ₂} diff --git a/src/Data/Sum/Relation/Binary/Pointwise.agda b/src/Data/Sum/Relation/Binary/Pointwise.agda index 2b9b4d763d..6e0cc43397 100644 --- a/src/Data/Sum/Relation/Binary/Pointwise.agda +++ b/src/Data/Sum/Relation/Binary/Pointwise.agda @@ -14,8 +14,7 @@ open import Data.Sum.Properties open import Level using (_⊔_) open import Function.Base using (_∘_; id) open import Function.Inverse using (Inverse) -open import Relation.Nullary -import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Decidable.Core using (yes; no; map′) open import Relation.Binary open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) import Relation.Binary.PropositionalEquality.Properties as P @@ -70,10 +69,10 @@ module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} ⊎-decidable : Decidable ∼₁ → Decidable ∼₂ → Decidable (Pointwise ∼₁ ∼₂) - ⊎-decidable _≟₁_ _≟₂_ (inj₁ x) (inj₁ y) = Dec.map′ inj₁ drop-inj₁ (x ≟₁ y) + ⊎-decidable _≟₁_ _≟₂_ (inj₁ x) (inj₁ y) = map′ inj₁ drop-inj₁ (x ≟₁ y) ⊎-decidable _≟₁_ _≟₂_ (inj₁ x) (inj₂ y) = no λ() ⊎-decidable _≟₁_ _≟₂_ (inj₂ x) (inj₁ y) = no λ() - ⊎-decidable _≟₁_ _≟₂_ (inj₂ x) (inj₂ y) = Dec.map′ inj₂ drop-inj₂ (x ≟₂ y) + ⊎-decidable _≟₁_ _≟₂_ (inj₂ x) (inj₂ y) = map′ inj₂ drop-inj₂ (x ≟₂ y) module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂} {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {≈₁ : Rel A₁ ℓ₂} From d70bb88742283c253cc2fda5da7f6fb598ef4a5b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 08:04:22 +0100 Subject: [PATCH 20/57] simplified imports for `Data.These.*\' --- src/Data/These/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/These/Properties.agda b/src/Data/These/Properties.agda index e7111cfce1..89ba37866f 100644 --- a/src/Data/These/Properties.agda +++ b/src/Data/These/Properties.agda @@ -13,7 +13,7 @@ open import Data.These.Base open import Function.Base using (_∘_) open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.PropositionalEquality -open import Relation.Nullary.Decidable using (yes; no; map′; _×-dec_) +open import Relation.Nullary.Decidable.Core using (yes; no; map′; _×-dec_) ------------------------------------------------------------------------ -- Equality From bfed6be3a71c083f5f42841bc38d3da5bff39e79 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 08:08:59 +0100 Subject: [PATCH 21/57] simplified imports for `Data.Tree.AVL.*\' --- src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda | 2 +- src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda | 2 +- src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda | 4 ++-- src/Data/Tree/AVL/Relation/Unary/Any.agda | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda index 545a925f00..5ff61463fa 100644 --- a/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda +++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda @@ -21,7 +21,7 @@ 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 using (Dec; yes; map′; _×-dec_) +open import Relation.Nullary.Decidable.Core using (Dec; yes; map′; _×-dec_) open import Relation.Unary using (Pred; Decidable; Universal; Irrelevant; _⊆_; _∪_) open StrictTotalOrder strictTotalOrder renaming (Carrier to Key) diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda index f8c270f1a1..47e6950060 100644 --- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda +++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda @@ -18,7 +18,7 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) open import Function.Base using (_∘′_; _∘_) open import Level using (Level; _⊔_) -open import Relation.Nullary.Decidable using (Dec; no; map′; _⊎-dec_) +open import Relation.Nullary.Decidable.Core using (Dec; no; map′; _⊎-dec_) open import Relation.Unary open StrictTotalOrder strictTotalOrder renaming (Carrier to Key) diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda index 02a09a098e..66eb26f0c8 100644 --- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda +++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda @@ -23,8 +23,8 @@ open import Level using (Level) open import Relation.Binary.Definitions using (_Respects_; tri<; tri≈; tri>) open import Relation.Binary.PropositionalEquality.Core using (_≡_) renaming (refl to ≡-refl) -open import Relation.Nullary using (¬_; Dec; yes; no) -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Decidable.Core using (Dec; yes; no) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Unary using (Pred; _∩_) open import Data.Tree.AVL.Indexed sto as AVL diff --git a/src/Data/Tree/AVL/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Relation/Unary/Any.agda index dfa96935ac..f57fd2e32f 100644 --- a/src/Data/Tree/AVL/Relation/Unary/Any.agda +++ b/src/Data/Tree/AVL/Relation/Unary/Any.agda @@ -16,7 +16,7 @@ open import Data.Product.Base as Prod using (∃) open import Function.Base using (_∘_; _$_) open import Level using (Level; _⊔_) -open import Relation.Nullary.Decidable using (map′) +open import Relation.Nullary.Decidable.Core using (map′) open import Relation.Unary open StrictTotalOrder strictTotalOrder renaming (Carrier to Key) From cc7e62ce51c0f5aac11719d481906dedb3cf7ce0 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 08:26:32 +0100 Subject: [PATCH 22/57] simplified imports for `Data.Vec.*\' --- src/Data/Vec/Functional/Properties.agda | 3 +-- src/Data/Vec/Membership/DecSetoid.agda | 2 +- src/Data/Vec/Properties.agda | 4 ++-- src/Data/Vec/Relation/Binary/Lex/Core.agda | 2 +- src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda | 7 +++---- src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda | 2 +- src/Data/Vec/Relation/Unary/All.agda | 4 ++-- src/Data/Vec/Relation/Unary/AllPairs.agda | 4 ++-- src/Data/Vec/Relation/Unary/Any.agda | 6 +++--- src/Data/Vec/Relation/Unary/Linked.agda | 2 +- src/Data/Vec/Relation/Unary/Linked/Properties.agda | 2 +- .../Relation/Unary/Unique/Propositional/Properties.agda | 2 +- 12 files changed, 19 insertions(+), 21 deletions(-) diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda index d0dbc16cda..1d799cd2b5 100644 --- a/src/Data/Vec/Functional/Properties.agda +++ b/src/Data/Vec/Functional/Properties.agda @@ -23,8 +23,7 @@ open import Function.Base open import Level using (Level) open import Relation.Binary as B open import Relation.Binary.PropositionalEquality -open import Relation.Nullary.Decidable - using (Dec; does; yes; no; map′; _×-dec_) +open import Relation.Nullary.Decidable.Core using (yes; no; map′; _×-dec_) import Data.Fin.Properties as Finₚ diff --git a/src/Data/Vec/Membership/DecSetoid.agda b/src/Data/Vec/Membership/DecSetoid.agda index fac9138660..a48beafa3f 100644 --- a/src/Data/Vec/Membership/DecSetoid.agda +++ b/src/Data/Vec/Membership/DecSetoid.agda @@ -12,7 +12,7 @@ module Data.Vec.Membership.DecSetoid {c ℓ} (DS : DecSetoid c ℓ) where open import Data.Vec.Base using (Vec) open import Data.Vec.Relation.Unary.Any using (any?) -open import Relation.Nullary.Decidable using (Dec) +open import Relation.Nullary.Decidable.Core using (Dec) open DecSetoid DS renaming (Carrier to A) ------------------------------------------------------------------------ diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 49924a7b31..f3c1b8fd51 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -28,8 +28,8 @@ open import Relation.Binary hiding (Decidable) open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; _≗_; refl; sym; trans; cong; cong₂; subst; module ≡-Reasoning) open import Relation.Unary using (Pred; Decidable) -open import Relation.Nullary.Decidable using (Dec; does; yes; no; _×-dec_; map′) -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Decidable.Core using (Dec; does; yes; no; _×-dec_; map′) +open import Relation.Nullary.Negation.Core using (contradiction) open ≡-Reasoning diff --git a/src/Data/Vec/Relation/Binary/Lex/Core.agda b/src/Data/Vec/Relation/Binary/Lex/Core.agda index c091d0f98c..5e79bb5ed2 100644 --- a/src/Data/Vec/Relation/Binary/Lex/Core.agda +++ b/src/Data/Vec/Relation/Binary/Lex/Core.agda @@ -23,7 +23,7 @@ open import Relation.Binary.PropositionalEquality.Core as P 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.Negation +open import Relation.Nullary.Negation.Core using (¬_; contradiction) private variable diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda b/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda index c7b2b3d7ea..f4564b4618 100644 --- a/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda +++ b/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda @@ -22,8 +22,8 @@ open import Relation.Binary hiding (_⇔_) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) open import Relation.Binary.Construct.Closure.Transitive as Plus hiding (equivalent; map) -open import Relation.Nullary -import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Decidable.Core using (map′) +open import Relation.Nullary.Negation.Core using (¬_) private variable @@ -107,8 +107,7 @@ trans trns xs∼ys ys∼zs = ext λ i → decidable : ∀ {_∼_ : REL A B ℓ} → Decidable _∼_ → ∀ {n} → Decidable (Pointwise _∼_ {n = n}) -decidable dec xs ys = Dec.map - (Setoid.sym (⇔-setoid _) equivalent) +decidable dec xs ys = map′ inductive⇒extensional extensional⇒inductive (Inductive.decidable dec xs ys) isEquivalence : ∀ {_∼_ : Rel A ℓ} {n} → diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda index 85bd6df9da..7a39e02698 100644 --- a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda +++ b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda @@ -18,7 +18,7 @@ open import Function.Base using (_∘_) open import Function.Bundles using (_⇔_; mk⇔) open import Relation.Binary open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) -open import Relation.Nullary.Decidable using (yes; no; _×-dec_; map′) +open import Relation.Nullary.Decidable.Core using (yes; no; _×-dec_; map′) open import Relation.Unary using (Pred) private diff --git a/src/Data/Vec/Relation/Unary/All.agda b/src/Data/Vec/Relation/Unary/All.agda index e8d24fbd65..9292e533eb 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.Core using (_×-dec_; yes; no; map′) 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) = map′ (uncurry _∷_) uncons (P? x ×-dec all? P? xs) universal : Universal P → ∀ {n} → Universal (All P {n}) universal u [] = [] diff --git a/src/Data/Vec/Relation/Unary/AllPairs.agda b/src/Data/Vec/Relation/Unary/AllPairs.agda index a702a1dbf9..8c85f24151 100644 --- 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 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.Core using (yes; no; _×-dec_; map′) ------------------------------------------------------------------------ -- 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) + map′ (uncurry _∷_) uncons (All.all? (R? x) xs ×-dec allPairs? R? xs) irrelevant : ∀ {n} → B.Irrelevant R → U.Irrelevant (AllPairs R {n}) irrelevant irr [] [] = refl diff --git a/src/Data/Vec/Relation/Unary/Any.agda b/src/Data/Vec/Relation/Unary/Any.agda index de901fe571..29ac2876e0 100644 --- a/src/Data/Vec/Relation/Unary/Any.agda +++ b/src/Data/Vec/Relation/Unary/Any.agda @@ -15,8 +15,8 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) open import Data.Vec.Base as Vec using (Vec; []; [_]; _∷_) open import Data.Product.Base as Prod using (∃; _,_) open import Level using (Level; _⊔_) -open import Relation.Nullary.Negation using (¬_; contradiction) -open import Relation.Nullary.Decidable as Dec using (yes; no; _⊎-dec_) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) +open import Relation.Nullary.Decidable.Core using (yes; no; _⊎-dec_; map′) open import Relation.Unary private @@ -76,7 +76,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) = map′ fromSum toSum (P? x ⊎-dec any? P? xs) satisfiable : Satisfiable P → ∀ {n} → Satisfiable (Any P {suc n}) satisfiable (x , p) {zero} = x ∷ [] , here p diff --git a/src/Data/Vec/Relation/Unary/Linked.agda b/src/Data/Vec/Relation/Unary/Linked.agda index 368c22ddc1..1184786ec8 100644 --- a/src/Data/Vec/Relation/Unary/Linked.agda +++ b/src/Data/Vec/Relation/Unary/Linked.agda @@ -19,7 +19,7 @@ open import Relation.Binary.Definitions as B open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_) open import Relation.Binary.PropositionalEquality 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.Core using (yes; no; _×-dec_; map′) private variable diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda index c32e4c8df6..eb2010a706 100644 --- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda @@ -24,7 +24,7 @@ open import Relation.Binary.Definitions using (Transitive) open import Relation.Binary.Bundles using (DecSetoid) open import Relation.Binary.PropositionalEquality.Core using (_≢_) open import Relation.Unary using (Pred; Decidable) -open import Relation.Nullary.Decidable using (yes; no; does) + private variable diff --git a/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda index 8e1fe54b4f..6ba412c596 100644 --- a/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda @@ -25,7 +25,7 @@ open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.PropositionalEquality using (refl; _≡_; _≢_; sym; setoid) open import Relation.Unary using (Pred; Decidable) -open import Relation.Nullary.Negation using (¬_) +open import Relation.Nullary.Negation.Core using (¬_) private variable From b2a5ac8ed3386175fe4a6f7bdf971da2fe392a95 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 08:27:19 +0100 Subject: [PATCH 23/57] simplified imports for `Data.Word.*\' --- src/Data/Word/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Word/Properties.agda b/src/Data/Word/Properties.agda index 3f9ad94ef1..f96d2bc32d 100644 --- a/src/Data/Word/Properties.agda +++ b/src/Data/Word/Properties.agda @@ -13,7 +13,7 @@ open import Data.Bool.Base using (Bool) open import Data.Word.Base import Data.Nat.Properties as ℕₚ open import Function.Base -open import Relation.Nullary.Decidable using (map′; ⌊_⌋) +open import Relation.Nullary.Decidable.Core using (map′; ⌊_⌋) open import Relation.Binary using ( _⇒_; Reflexive; Symmetric; Transitive; Substitutive ; Decidable; DecidableEquality; IsEquivalence; IsDecEquivalence From 060d2d766ecb96665cd46687ec2ec0d1de334734 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 08:30:07 +0100 Subject: [PATCH 24/57] simplified imports for `Effect.Monad.Partiality\' --- src/Effect/Monad/Partiality.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Effect/Monad/Partiality.agda b/src/Effect/Monad/Partiality.agda index 194b079339..8bd965acd9 100644 --- a/src/Effect/Monad/Partiality.agda +++ b/src/Effect/Monad/Partiality.agda @@ -29,8 +29,7 @@ open import Relation.Binary.Bundles import Relation.Binary.Properties.Setoid as SetoidProperties open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) import Relation.Binary.PropositionalEquality.Properties as P -open import Relation.Nullary -open import Relation.Nullary.Decidable hiding (map) +open import Relation.Nullary.Decidable.Core open import Relation.Nullary.Negation private From f621e5e1b547ad5dd4d20019dab3f2682e071d24 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 08:35:19 +0100 Subject: [PATCH 25/57] tweak use of `invert` --- src/Function/Related/TypeIsomorphisms.agda | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda index 9922c69fcf..775502e16c 100644 --- a/src/Function/Related/TypeIsomorphisms.agda +++ b/src/Function/Related/TypeIsomorphisms.agda @@ -30,10 +30,9 @@ open import Function.Inverse as Inv using (_↔_; Inverse; inverse) open import Function.Related open import Relation.Binary hiding (_⇔_) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) -open import Relation.Nullary.Reflects using (invert) -open import Relation.Nullary using (Dec; ¬_; _because_; ofⁿ) +open import Relation.Nullary.Decidable.Core using (Dec; yes; no; True) import Relation.Nullary.Indexed as I -open import Relation.Nullary.Decidable using (True) +open import Relation.Nullary.Negation.Core using (¬_) ------------------------------------------------------------------------ -- Properties of Σ and _×_ @@ -332,10 +331,10 @@ Related-cong {A = A} {B} {C} {D} A≈B C≈D = True↔ : ∀ {p} {P : Set p} (dec : Dec P) → ((p₁ p₂ : P) → p₁ ≡ p₂) → True dec ↔ P -True↔ ( true because [p]) irr = - inverse (λ _ → invert [p]) (λ _ → _) (λ _ → P.refl) (irr _) -True↔ (false because ofⁿ ¬p) _ = - inverse (λ()) (invert (ofⁿ ¬p)) (λ ()) (⊥-elim ∘ ¬p) +True↔ (yes p) irr = + inverse (λ _ → p) (λ _ → _) (λ _ → P.refl) (irr _) +True↔ (no ¬p) _ = + inverse (λ()) ¬p (λ ()) (⊥-elim ∘ ¬p) ------------------------------------------------------------------------ -- Equality between pairs can be expressed as a pair of equalities From 741e437334bcd990f9fb74d708c8486c4a9395b7 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 09:02:47 +0100 Subject: [PATCH 26/57] simplified imports for `Relation.*ary.*\' --- src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda | 5 ++--- src/Relation/Binary/Construct/Add/Infimum/Strict.agda | 5 ++--- src/Relation/Binary/Construct/Add/Point/Equality.agda | 5 ++--- src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda | 5 ++--- src/Relation/Binary/Construct/Add/Supremum/Strict.agda | 5 ++--- .../Binary/Construct/Closure/Reflexive/Properties.agda | 6 +++--- src/Relation/Binary/Construct/Intersection.agda | 2 +- src/Relation/Binary/Construct/NonStrictToStrict.agda | 5 ++--- src/Relation/Binary/Construct/StrictToNonStrict.agda | 2 +- src/Relation/Binary/Construct/Union.agda | 2 +- src/Relation/Binary/Morphism/RelMonomorphism.agda | 3 +-- src/Relation/Binary/Reasoning/Base/Apartness.agda | 3 +-- src/Relation/Binary/Reasoning/Base/Partial.agda | 3 +-- src/Relation/Binary/Reasoning/Base/Single.agda | 2 +- src/Relation/Nary.agda | 8 ++++---- src/Relation/Unary/Polymorphic/Properties.agda | 2 +- src/Relation/Unary/Properties.agda | 2 +- 17 files changed, 28 insertions(+), 37 deletions(-) diff --git a/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda b/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda index b6cd5e4bf6..e9e3925a63 100644 --- a/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda +++ b/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda @@ -20,9 +20,8 @@ open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl) import Relation.Binary.PropositionalEquality.Properties as P import Relation.Binary.Construct.Add.Infimum.Equality as Equality -open import Relation.Nullary hiding (Irrelevant) open import Relation.Nullary.Construct.Add.Infimum -import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Decidable.Core using (yes; no; map′) ------------------------------------------------------------------------ -- Definition @@ -48,7 +47,7 @@ data _≤₋_ : Rel (A ₋) (a ⊔ ℓ) where ≤₋-dec : Decidable _≤_ → Decidable _≤₋_ ≤₋-dec _≤?_ ⊥₋ l = yes (⊥₋≤ l) ≤₋-dec _≤?_ [ k ] ⊥₋ = no (λ ()) -≤₋-dec _≤?_ [ k ] [ l ] = Dec.map′ [_] [≤]-injective (k ≤? l) +≤₋-dec _≤?_ [ k ] [ l ] = map′ [_] [≤]-injective (k ≤? l) ≤₋-total : Total _≤_ → Total _≤₋_ ≤₋-total ≤-total ⊥₋ l = inj₁ (⊥₋≤ l) diff --git a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda index e4c8f3a974..5d9d406f0e 100644 --- a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda +++ b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda @@ -22,9 +22,8 @@ open import Relation.Binary.PropositionalEquality.Core as P import Relation.Binary.PropositionalEquality.Properties as P import Relation.Binary.Construct.Add.Infimum.Equality as Equality import Relation.Binary.Construct.Add.Infimum.NonStrict as NonStrict -open import Relation.Nullary hiding (Irrelevant) open import Relation.Nullary.Construct.Add.Infimum -import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Decidable.Core ------------------------------------------------------------------------ -- Definition @@ -52,7 +51,7 @@ data _<₋_ : Rel (A ₋) (a ⊔ ℓ) where <₋-dec _ _ _ c = inj₂ [ c ] dec : Decidable {A = A} _≡_ → Decidable _~_ → Decidable _~ᵒ_ - dec ≡-dec ~-dec a b = Dec.map ⊎⇔Refl (≡-dec a b ⊎-dec ~-dec a b) + dec ≡-dec ~-dec a b = map′ fromSum toSum (≡-dec a b ⊎-dec ~-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 17845536ca..45ce7a7bc1 100644 --- a/src/Relation/Binary/Construct/Intersection.agda +++ b/src/Relation/Binary/Construct/Intersection.agda @@ -13,7 +13,7 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]) open import Function.Base using (_∘_) open import Level using (Level; _⊔_) open import Relation.Binary -open import Relation.Nullary.Decidable using (yes; no; _×-dec_) +open import Relation.Nullary.Decidable.Core using (yes; no; _×-dec_) private variable diff --git a/src/Relation/Binary/Construct/NonStrictToStrict.agda b/src/Relation/Binary/Construct/NonStrictToStrict.agda index d9dd2c57ce..319554317c 100644 --- a/src/Relation/Binary/Construct/NonStrictToStrict.agda +++ b/src/Relation/Binary/Construct/NonStrictToStrict.agda @@ -14,9 +14,8 @@ module Relation.Binary.Construct.NonStrictToStrict 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.Negation using (contradiction) -open import Relation.Nullary.Decidable using (¬?; _×-dec_) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) +open import Relation.Nullary.Decidable.Core using (yes; no; ¬?; _×-dec_) private _≉_ : Rel A ℓ₁ diff --git a/src/Relation/Binary/Construct/StrictToNonStrict.agda b/src/Relation/Binary/Construct/StrictToNonStrict.agda index 42c76fc80f..aebc91613a 100644 --- a/src/Relation/Binary/Construct/StrictToNonStrict.agda +++ b/src/Relation/Binary/Construct/StrictToNonStrict.agda @@ -22,7 +22,7 @@ open import Data.Sum.Base open import Data.Empty open import Function.Base open import Relation.Binary.Consequences -open import Relation.Nullary.Decidable using (_⊎-dec_; yes; no) +open import Relation.Nullary.Decidable.Core using (_⊎-dec_; yes; no) ------------------------------------------------------------------------ -- Conversion diff --git a/src/Relation/Binary/Construct/Union.agda b/src/Relation/Binary/Construct/Union.agda index 2b70ce8500..c302f9ea1f 100644 --- a/src/Relation/Binary/Construct/Union.agda +++ b/src/Relation/Binary/Construct/Union.agda @@ -13,7 +13,7 @@ open import Data.Sum.Base as Sum open import Function.Base using (_∘_) open import Level using (Level; _⊔_) open import Relation.Binary -open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_) +open import Relation.Nullary.Decidable.Core using (yes; no; _⊎-dec_) private variable diff --git a/src/Relation/Binary/Morphism/RelMonomorphism.agda b/src/Relation/Binary/Morphism/RelMonomorphism.agda index e500fa4368..c655d7bb2f 100644 --- a/src/Relation/Binary/Morphism/RelMonomorphism.agda +++ b/src/Relation/Binary/Morphism/RelMonomorphism.agda @@ -20,8 +20,7 @@ module Relation.Binary.Morphism.RelMonomorphism where open import Data.Sum.Base as Sum -open import Relation.Nullary.Decidable using (yes; no) -open import Relation.Nullary.Decidable +open import Relation.Nullary.Decidable.Core using (yes; no; map′) open IsRelMonomorphism isMonomorphism diff --git a/src/Relation/Binary/Reasoning/Base/Apartness.agda b/src/Relation/Binary/Reasoning/Base/Apartness.agda index 7a52568664..893aa0c362 100644 --- a/src/Relation/Binary/Reasoning/Base/Apartness.agda +++ b/src/Relation/Binary/Reasoning/Base/Apartness.agda @@ -19,8 +19,7 @@ module Relation.Binary.Reasoning.Base.Apartness {a ℓ₁ ℓ₂} {A : Set a} open import Level using (Level; _⊔_) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym) -open import Relation.Nullary.Decidable using (Dec; yes; no) -open import Relation.Nullary.Decidable using (True; toWitness) +open import Relation.Nullary.Decidable.Core using (Dec; yes; no; True; toWitness) open IsEquivalence ≈-equiv renaming diff --git a/src/Relation/Binary/Reasoning/Base/Partial.agda b/src/Relation/Binary/Reasoning/Base/Partial.agda index e53f7e4efe..72938d9d64 100644 --- a/src/Relation/Binary/Reasoning/Base/Partial.agda +++ b/src/Relation/Binary/Reasoning/Base/Partial.agda @@ -11,8 +11,7 @@ open import Relation.Binary.Definitions open import Level using (_⊔_) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) -open import Relation.Nullary.Decidable using (Dec; yes; no) -open import Relation.Nullary.Decidable using (True) +open import Relation.Nullary.Decidable.Core using (Dec; yes; no; True) module Relation.Binary.Reasoning.Base.Partial {a ℓ} {A : Set a} (_∼_ : Rel A ℓ) (trans : Transitive _∼_) diff --git a/src/Relation/Binary/Reasoning/Base/Single.agda b/src/Relation/Binary/Reasoning/Base/Single.agda index 97da6b06b8..ab854805ad 100644 --- a/src/Relation/Binary/Reasoning/Base/Single.agda +++ b/src/Relation/Binary/Reasoning/Base/Single.agda @@ -15,7 +15,7 @@ module Relation.Binary.Reasoning.Base.Single -- TODO: the following part is copied from Relation.Binary.Reasoning.Base.Partial -- in order to avoid larger refactors. We will refactor this part later --- so taht we use the same framework as Relation.Binary.Reasoning.Base.Partial. +-- so that we use the same framework as Relation.Binary.Reasoning.Base.Partial. open import Level using (_⊔_) open import Relation.Binary.PropositionalEquality.Core as P diff --git a/src/Relation/Nary.agda b/src/Relation/Nary.agda index 6610b16439..c97df4062c 100644 --- a/src/Relation/Nary.agda +++ b/src/Relation/Nary.agda @@ -24,8 +24,8 @@ open import Data.Product.Nary.NonDependent open import Data.Sum.Base using (_⊎_) open import Function.Base using (_$_; _∘′_) open import Function.Nary.NonDependent -open import Relation.Nullary.Negation using (¬_) -open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _because_; _×-dec_) +open import Relation.Nullary.Negation.Core using (¬_) +open import Relation.Nullary.Decidable.Core hiding (⌊_⌋; toWitness; fromWitness) import Relation.Unary as Unary open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst) @@ -85,7 +85,7 @@ infix 5 ∃⟨_⟩ Π[_] ∀[_] ∀ {l r} → Arrows n (Dec <$> Equalₙ n l r) (Dec (uncurryₙ n con l ≡ uncurryₙ n con r)) ≟-mapₙ n con con-inj = curryₙ n λ a?s → let as? = Product-dec n a?s in - Dec.map′ (cong (uncurryₙ n con) ∘′ fromEqualₙ n) con-inj as? + map′ (cong (uncurryₙ n con) ∘′ fromEqualₙ n) con-inj as? ------------------------------------------------------------------------ -- Substitution @@ -187,7 +187,7 @@ Decidable R = Π[ mapₙ _ Dec R ] -- erasure ⌊_⌋ : ∀ {n ls r} {as : Sets n ls} {R : as ⇉ Set r} → Decidable R → as ⇉ Set r -⌊_⌋ {zero} R? = Lift _ (Dec.True R?) +⌊_⌋ {zero} R? = Lift _ (True R?) ⌊_⌋ {suc n} R? a = ⌊ R? a ⌋ -- equivalence between R and its erasure diff --git a/src/Relation/Unary/Polymorphic/Properties.agda b/src/Relation/Unary/Polymorphic/Properties.agda index 3a59912e2b..d364830ff3 100644 --- a/src/Relation/Unary/Polymorphic/Properties.agda +++ b/src/Relation/Unary/Polymorphic/Properties.agda @@ -11,7 +11,7 @@ module Relation.Unary.Polymorphic.Properties where open import Level using (Level) open import Relation.Binary.Definitions hiding (Decidable; Universal) -open import Relation.Nullary.Decidable using (yes; no) +open import Relation.Nullary.Decidable.Core using (yes; no) open import Relation.Unary hiding (∅; U) open import Relation.Unary.Polymorphic open import Data.Unit.Polymorphic.Base using (tt) diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda index d090716c08..87dc933e41 100644 --- a/src/Relation/Unary/Properties.agda +++ b/src/Relation/Unary/Properties.agda @@ -16,7 +16,7 @@ open import Relation.Binary.Core as Binary open import Relation.Binary.Definitions hiding (Decidable; Universal; Irrelevant) open import Relation.Binary.PropositionalEquality.Core using (refl) open import Relation.Unary -open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_; ¬?) +open import Relation.Nullary.Decidable.Core using (yes; no; _⊎-dec_; _×-dec_; ¬?) open import Function.Base using (id; _$_; _∘_) private From 72e5159ef341992c288d2c1f1c060153f780442c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 09:03:36 +0100 Subject: [PATCH 27/57] removed imports for `System.Clock` --- src/System/Clock.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/System/Clock.agda b/src/System/Clock.agda index d8b8745b17..9dae2e2e9c 100644 --- a/src/System/Clock.agda +++ b/src/System/Clock.agda @@ -21,7 +21,6 @@ open import IO.Base open import Function.Base using (_$_; _∘′_) open import Foreign.Haskell using (_,_) -open import Relation.Nullary.Decidable using (False; fromWitnessFalse; toWitnessFalse) private variable From f0114fa50f6de39bec282ca712477c5d7feeb5b7 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 09:05:48 +0100 Subject: [PATCH 28/57] simplified imports for `tests.*\' --- tests/data/trie/Main.agda | 2 +- tests/reflection/assumption/Main.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/data/trie/Main.agda b/tests/data/trie/Main.agda index 3ce2ad3ecb..2c1feaa7cd 100644 --- a/tests/data/trie/Main.agda +++ b/tests/data/trie/Main.agda @@ -19,7 +19,7 @@ open import Data.These as These open import Function.Base using (case_of_; _$_; _∘′_; id; _on_) open import Relation.Nary open import Relation.Binary.Core using (Rel) -open import Relation.Nullary.Decidable using (¬?) +open import Relation.Nullary.Decidable.Core using (¬?) open import Data.Trie Char.<-strictTotalOrder open import Data.Tree.AVL.Value diff --git a/tests/reflection/assumption/Main.agda b/tests/reflection/assumption/Main.agda index cf0d21b514..5663c0b524 100644 --- a/tests/reflection/assumption/Main.agda +++ b/tests/reflection/assumption/Main.agda @@ -17,7 +17,7 @@ open import Reflection.AST.Literal hiding (_≟_) open import Reflection.AST.Argument using (Arg; unArg; arg) open import Reflection.AST.DeBruijn open import Reflection.AST.Show -open import Relation.Nullary.Decidable using (does) +open import Relation.Nullary.Decidable.Core using (does) open import Effect.Monad open RawMonad {{...}} From bcaac546ff5264afefaefc2270bf5cde426a50f4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 09:07:02 +0100 Subject: [PATCH 29/57] simplified imports for `Tactic.*\' --- src/Tactic/RingSolver.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Tactic/RingSolver.agda b/src/Tactic/RingSolver.agda index 07e9f1a033..c3cdbaf1ca 100644 --- a/src/Tactic/RingSolver.agda +++ b/src/Tactic/RingSolver.agda @@ -20,7 +20,7 @@ open import Data.Unit.Base using (⊤) open import Data.String.Base as String using (String; _++_; parens) open import Data.Product.Base using (_,_; proj₁) open import Function.Base -open import Relation.Nullary.Decidable +open import Relation.Nullary.Decidable.Core open import Reflection open import Reflection.AST.Argument From 14a50e440d67b5df1415d849f9d845d526ffea46 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 09:08:03 +0100 Subject: [PATCH 30/57] simplified imports for `Test.*\' --- src/Test/Golden.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Test/Golden.agda b/src/Test/Golden.agda index 43bbd3037e..7e592a3ff2 100644 --- a/src/Test/Golden.agda +++ b/src/Test/Golden.agda @@ -97,7 +97,7 @@ open import Data.Unit.Base using (⊤) open import Function.Base using (id; _$_; case_of_) -open import Relation.Nullary.Decidable using (does) +open import Relation.Nullary.Decidable.Core using (does) open import Codata.Musical.Notation using (♯_) open import IO From 332880f69960ff37125a43bd84465d573fa9c0cd Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 09:13:36 +0100 Subject: [PATCH 31/57] simplified imports for `Text.Regex.*\' --- src/Text/Pretty/Core.agda | 2 +- src/Text/Regex/Derivative/Brzozowski.agda | 5 ++--- src/Text/Regex/Properties.agda | 4 ++-- src/Text/Regex/Search.agda | 5 ++--- src/Text/Regex/SmartConstructors.agda | 4 ++-- src/Text/Regex/String/Unsafe.agda | 2 +- 6 files changed, 10 insertions(+), 12 deletions(-) diff --git a/src/Text/Pretty/Core.agda b/src/Text/Pretty/Core.agda index 974b1af823..8dd947e958 100644 --- a/src/Text/Pretty/Core.agda +++ b/src/Text/Pretty/Core.agda @@ -33,7 +33,7 @@ open import Data.String.Base as String using (String; length; replicate; _++_; unlines) open import Data.String.Unsafe as Stringₚ open import Function.Base -open import Relation.Nullary.Decidable using (Dec) +open import Relation.Nullary.Decidable.Core using (Dec) open import Relation.Unary using (IUniversal; _⇒_; U) open import Relation.Binary.PropositionalEquality diff --git a/src/Text/Regex/Derivative/Brzozowski.agda b/src/Text/Regex/Derivative/Brzozowski.agda index 9c66c831a4..3b2861b06d 100644 --- a/src/Text/Regex/Derivative/Brzozowski.agda +++ b/src/Text/Regex/Derivative/Brzozowski.agda @@ -15,9 +15,8 @@ open import Data.List.Relation.Binary.Equality.Propositional open import Data.Sum.Base as Sum using (inj₁; inj₂) open import Function.Base using (_$_; _∘′_; case_of_) -open import Relation.Nullary.Decidable using (Dec; yes; no) -open import Relation.Nullary.Negation using (contradiction) -open import Relation.Nullary.Decidable using (map′; ¬?) +open import Relation.Nullary.Decidable.Core using (Dec; yes; no; map′; ¬?) +open import Relation.Nullary.Negation.Core using (contradiction) open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong) diff --git a/src/Text/Regex/Properties.agda b/src/Text/Regex/Properties.agda index 02b6db2039..48b073ee22 100644 --- a/src/Text/Regex/Properties.agda +++ b/src/Text/Regex/Properties.agda @@ -17,9 +17,9 @@ open import Data.Product.Base using (_×_; _,_; uncurry) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Function.Base using (_$_) -open import Relation.Nullary.Decidable +open import Relation.Nullary.Decidable.Core using (Dec; yes; no; map′; ¬?; _×-dec_; _⊎-dec_) -open import Relation.Nullary.Negation +open import Relation.Nullary.Negation.Core using (¬_; contradiction) import Relation.Unary as U diff --git a/src/Text/Regex/Search.agda b/src/Text/Regex/Search.agda index efa1f74684..7c6ce741a5 100644 --- a/src/Text/Regex/Search.agda +++ b/src/Text/Regex/Search.agda @@ -26,9 +26,8 @@ open import Data.List.Relation.Binary.Pointwise open import Data.List.Relation.Binary.Suffix.Heterogeneous using (Suffix; here; there) hiding (module Suffix) -open import Relation.Nullary using (Dec; ¬_; yes; no) -open import Relation.Nullary.Decidable using (map′) -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Decidable.Core using (Dec; yes; no; map′) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Binary.Core using (Rel; _⇒_) open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.PropositionalEquality.Core diff --git a/src/Text/Regex/SmartConstructors.agda b/src/Text/Regex/SmartConstructors.agda index 3269d22da5..5d7d8a04d2 100644 --- a/src/Text/Regex/SmartConstructors.agda +++ b/src/Text/Regex/SmartConstructors.agda @@ -17,8 +17,8 @@ open import Data.List.Base using ([]) open import Data.List.Relation.Ternary.Appending.Propositional open import Data.Sum.Base using (inj₁; inj₂; fromInj₁; fromInj₂) -open import Relation.Nullary.Decidable using (yes; no) -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Decidable.Core using (yes; no) +open import Relation.Nullary.Negation.Core using (contradiction) open import Relation.Binary.PropositionalEquality.Core using (refl) open import Text.Regex.Base P as R hiding (_∣_; _∙_; _⋆) diff --git a/src/Text/Regex/String/Unsafe.agda b/src/Text/Regex/String/Unsafe.agda index 118b48505a..ef04bd44a1 100644 --- a/src/Text/Regex/String/Unsafe.agda +++ b/src/Text/Regex/String/Unsafe.agda @@ -15,7 +15,7 @@ open import Level using (0ℓ) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.PropositionalEquality.Core using (_≡_; sym; subst) -open import Relation.Nullary.Decidable using (map′) +open import Relation.Nullary.Decidable.Core using (map′) ------------------------------------------------------------------------ -- Re-exporting safe definitions From b86106c1648bde55c26807648a203e0f9185d2d9 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 09:19:57 +0100 Subject: [PATCH 32/57] simplified imports for `Reflection.AST.*\' --- src/Reflection/AST/Abstraction.agda | 2 +- src/Reflection/AST/AlphaEquality.agda | 12 ++++++------ src/Reflection/AST/Argument.agda | 2 +- src/Reflection/AST/Argument/Information.agda | 2 +- src/Reflection/AST/Argument/Modality.agda | 2 +- src/Reflection/AST/Argument/Quantity.agda | 2 +- src/Reflection/AST/Argument/Relevance.agda | 2 +- src/Reflection/AST/Argument/Visibility.agda | 2 +- src/Reflection/AST/Definition.agda | 2 +- src/Reflection/AST/Literal.agda | 2 +- src/Reflection/AST/Meta.agda | 2 +- src/Reflection/AST/Name.agda | 2 +- src/Reflection/AST/Show.agda | 2 +- src/Reflection/AST/Term.agda | 2 +- 14 files changed, 19 insertions(+), 19 deletions(-) diff --git a/src/Reflection/AST/Abstraction.agda b/src/Reflection/AST/Abstraction.agda index 43fb2f8302..07c4d2da11 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 -open import Relation.Nullary.Decidable using (Dec; map′; _×-dec_) +open import Relation.Nullary.Decidable.Core using (Dec; map′; _×-dec_) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂) diff --git a/src/Reflection/AST/AlphaEquality.agda b/src/Reflection/AST/AlphaEquality.agda index 4849470d50..1584471bcc 100644 --- a/src/Reflection/AST/AlphaEquality.agda +++ b/src/Reflection/AST/AlphaEquality.agda @@ -8,12 +8,12 @@ module Reflection.AST.AlphaEquality where -open import Data.Bool.Base using (Bool; true; false; _∧_) -open import Data.List.Base using ([]; _∷_) -open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _≡ᵇ_) -open import Data.Product.Base using (_,_) -open import Relation.Nullary.Decidable using (⌊_⌋) -open import Relation.Binary.Definitions using (DecidableEquality) +open import Data.Bool.Base using (Bool; true; false; _∧_) +open import Data.List.Base using ([]; _∷_) +open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _≡ᵇ_) +open import Data.Product.Base using (_,_) +open import Relation.Nullary.Decidable.Core using (⌊_⌋) +open import Relation.Binary.Definitions using (DecidableEquality) open import Reflection.AST.Abstraction open import Reflection.AST.Argument diff --git a/src/Reflection/AST/Argument.agda b/src/Reflection/AST/Argument.agda index b97ec90f77..d21b3688cb 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 using (Dec; map′; _×-dec_) +open import Relation.Nullary.Decidable.Core using (Dec; map′; _×-dec_) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂) open import Level diff --git a/src/Reflection/AST/Argument/Information.agda b/src/Reflection/AST/Argument/Information.agda index 66fec3be77..98c91ee818 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 using (map′; _×-dec_) +open import Relation.Nullary.Decidable.Core using (map′; _×-dec_) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂) diff --git a/src/Reflection/AST/Argument/Modality.agda b/src/Reflection/AST/Argument/Modality.agda index 489247031e..722c1cfa0e 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 using (map′; _×-dec_) +open import Relation.Nullary.Decidable.Core using (map′; _×-dec_) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂) diff --git a/src/Reflection/AST/Argument/Quantity.agda b/src/Reflection/AST/Argument/Quantity.agda index bc79d74b3c..9eee622b67 100644 --- a/src/Reflection/AST/Argument/Quantity.agda +++ b/src/Reflection/AST/Argument/Quantity.agda @@ -8,7 +8,7 @@ module Reflection.AST.Argument.Quantity where -open import Relation.Nullary using (yes; no) +open import Relation.Nullary.Decidable.Core using (yes; no) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (refl) diff --git a/src/Reflection/AST/Argument/Relevance.agda b/src/Reflection/AST/Argument/Relevance.agda index 3ac78cf765..b2ef362d7d 100644 --- a/src/Reflection/AST/Argument/Relevance.agda +++ b/src/Reflection/AST/Argument/Relevance.agda @@ -8,7 +8,7 @@ module Reflection.AST.Argument.Relevance where -open import Relation.Nullary using (yes; no) +open import Relation.Nullary.Decidable.Core using (yes; no) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (refl) diff --git a/src/Reflection/AST/Argument/Visibility.agda b/src/Reflection/AST/Argument/Visibility.agda index b384609c93..f8bd2afeee 100644 --- a/src/Reflection/AST/Argument/Visibility.agda +++ b/src/Reflection/AST/Argument/Visibility.agda @@ -8,7 +8,7 @@ module Reflection.AST.Argument.Visibility where -open import Relation.Nullary using (yes; no) +open import Relation.Nullary.Decidable.Core using (yes; no) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (refl) diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda index b5b5b32700..b97fe47cae 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 using (map′; _×-dec_; yes; no) +open import Relation.Nullary.Decidable.Core using (map′; _×-dec_; yes; no) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂) diff --git a/src/Reflection/AST/Literal.agda b/src/Reflection/AST/Literal.agda index 00ac5cc652..9976d5d52f 100644 --- a/src/Reflection/AST/Literal.agda +++ b/src/Reflection/AST/Literal.agda @@ -17,7 +17,7 @@ import Data.Word as Word using (_≟_) import Reflection.AST.Meta as Meta import Reflection.AST.Name as Name open import Relation.Nullary using (yes; no) -open import Relation.Nullary.Decidable using (map′; isYes) +open import Relation.Nullary.Decidable.Core using (map′; isYes) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong) diff --git a/src/Reflection/AST/Meta.agda b/src/Reflection/AST/Meta.agda index 682a52c8ca..2171a90ed0 100644 --- a/src/Reflection/AST/Meta.agda +++ b/src/Reflection/AST/Meta.agda @@ -10,7 +10,7 @@ module Reflection.AST.Meta where import Data.Nat.Properties as ℕₚ using (_≟_) open import Function.Base using (_on_) -open import Relation.Nullary.Decidable using (map′) +open import Relation.Nullary.Decidable.Core using (map′) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Definitions using (Decidable; DecidableEquality) import Relation.Binary.Construct.On as On diff --git a/src/Reflection/AST/Name.agda b/src/Reflection/AST/Name.agda index ac478443fb..c386912f08 100644 --- a/src/Reflection/AST/Name.agda +++ b/src/Reflection/AST/Name.agda @@ -12,7 +12,7 @@ open import Data.List.Base using (List) import Data.Product.Properties as Prodₚ using (≡-dec) import Data.Word.Properties as Wₚ using (_≟_) open import Function.Base using (_on_) -open import Relation.Nullary.Decidable using (map′) +open import Relation.Nullary.Decidable.Core using (map′) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Definitions using (Decidable; DecidableEquality) open import Relation.Binary.Construct.On using (decidable) diff --git a/src/Reflection/AST/Show.agda b/src/Reflection/AST/Show.agda index efe77a4779..14fdf02684 100644 --- a/src/Reflection/AST/Show.agda +++ b/src/Reflection/AST/Show.agda @@ -20,7 +20,7 @@ open import Data.String as String using (parensIfSpace) open import Data.Product.Base using (_×_; _,_) import Data.Word as Word using (toℕ) open import Function.Base using (id; _∘′_; case_of_) -open import Relation.Nullary.Decidable using (yes; no) +open import Relation.Nullary.Decidable.Core using (yes; no) open import Reflection.AST.Abstraction hiding (map) open import Reflection.AST.Argument hiding (map) diff --git a/src/Reflection/AST/Term.agda b/src/Reflection/AST/Term.agda index 33ef68d6f0..f51d91b861 100644 --- a/src/Reflection/AST/Term.agda +++ b/src/Reflection/AST/Term.agda @@ -16,7 +16,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.Core using (map′; _×-dec_; yes; no) open import Relation.Binary.Definitions using (Decidable; DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂) From ccfec83114d59e854283249711fa2b7b771253b5 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 09:28:23 +0100 Subject: [PATCH 33/57] simplified imports for `README.*\' --- README/Axiom.agda | 2 +- README/Data/Trie/NonDependent.agda | 2 +- README/Design/Decidability.agda | 2 +- README/Foreign/Haskell.agda | 2 +- README/Text/Regex.agda | 3 +-- 5 files changed, 5 insertions(+), 6 deletions(-) diff --git a/README/Axiom.agda b/README/Axiom.agda index 43805af9c5..c60e08d207 100644 --- a/README/Axiom.agda +++ b/README/Axiom.agda @@ -31,7 +31,7 @@ private variable ℓ : Level -- The types for which `P` or `¬P` holds is called `Dec P` in the -- standard library (short for `Decidable`). -open import Relation.Nullary.Decidable using (Dec) +open import Relation.Nullary.Decidable.Core using (Dec) -- The type of the proof of saying that excluded middle holds for -- all types at universe level ℓ is therefore: diff --git a/README/Data/Trie/NonDependent.agda b/README/Data/Trie/NonDependent.agda index 0484e6005a..e70c378ae5 100644 --- a/README/Data/Trie/NonDependent.agda +++ b/README/Data/Trie/NonDependent.agda @@ -64,7 +64,7 @@ open import Data.These as These open import Function.Base using (case_of_; _$_; _∘′_; id; _on_) open import Relation.Nary open import Relation.Binary.Core using (Rel) -open import Relation.Nullary.Decidable using (¬?) +open import Relation.Nullary.Decidable.Core using (¬?) open import Data.Trie Char.<-strictTotalOrder open import Data.Tree.AVL.Value diff --git a/README/Design/Decidability.agda b/README/Design/Decidability.agda index c02eadad53..6fe452d416 100644 --- a/README/Design/Decidability.agda +++ b/README/Design/Decidability.agda @@ -42,7 +42,7 @@ ex₂ = T⁺ ------------------------------------------------------------------------ -- Dec -open import Relation.Nullary.Decidable +open import Relation.Nullary.Decidable.Core -- A proof of `Dec P` is a proof of `Reflects P b` for some `b`. -- `Dec P` is declared as a record, with fields: diff --git a/README/Foreign/Haskell.agda b/README/Foreign/Haskell.agda index 38c6c78c4e..9b2db72679 100644 --- a/README/Foreign/Haskell.agda +++ b/README/Foreign/Haskell.agda @@ -24,7 +24,7 @@ open import Data.List.Base as List using (List; _∷_; []; takeWhile; dropWhile) open import Data.Maybe.Base using (Maybe; just; nothing) open import Data.Product.Base using (_×_; _,_) open import Function -open import Relation.Nullary.Decidable +open import Relation.Nullary.Decidable.Core using (¬?) import Foreign.Haskell as FFI open import Foreign.Haskell.Coerce diff --git a/README/Text/Regex.agda b/README/Text/Regex.agda index 17d3fe45f9..a099f1cbab 100644 --- a/README/Text/Regex.agda +++ b/README/Text/Regex.agda @@ -12,8 +12,7 @@ open import Data.Bool using (true; false) open import Data.List.Base using (_∷_; []) open import Data.String open import Function.Base using () renaming (_$′_ to _$_) -open import Relation.Nullary.Decidable using (yes) -open import Relation.Nullary.Decidable using (True; False; from-yes) +open import Relation.Nullary.Decidable.Core using (yes; True; False; from-yes) -- Our library available via the Text.Regex module is safe but it works on -- lists of characters. From a00863ecdb48a39c14c416b9641f730652e6cb97 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 09:44:07 +0100 Subject: [PATCH 34/57] yet more simplified imports --- src/Data/Char/Properties.agda | 2 +- src/Data/Digit.agda | 2 +- src/Data/Digit/Properties.agda | 2 +- src/Data/Fin/Induction.agda | 4 ++-- src/Data/Fin/Literals.agda | 6 +++--- src/Data/Fin/Show.agda | 3 +-- src/Data/Fin/Subset/Properties.agda | 20 +++++++++++--------- 7 files changed, 20 insertions(+), 19 deletions(-) diff --git a/src/Data/Char/Properties.agda b/src/Data/Char/Properties.agda index 52a997fd81..50565ebdf2 100644 --- a/src/Data/Char/Properties.agda +++ b/src/Data/Char/Properties.agda @@ -16,7 +16,7 @@ open import Data.Product.Base using (_,_) open import Function.Base open import Relation.Nullary using (¬_; yes; no) -open import Relation.Nullary.Decidable using (map′; isYes) +open import Relation.Nullary.Decidable.Core using (map′; isYes) open import Relation.Binary import Relation.Binary.Construct.On as On import Relation.Binary.Construct.Subst.Equality as Subst diff --git a/src/Data/Digit.agda b/src/Data/Digit.agda index 60557b142a..9bbd3cb779 100644 --- a/src/Data/Digit.agda +++ b/src/Data/Digit.agda @@ -19,7 +19,7 @@ open import Data.Product.Base using (∃; _,_) open import Data.Vec.Base as Vec using (Vec; _∷_; []) open import Data.Nat.DivMod open import Data.Nat.Induction -open import Relation.Nullary.Decidable using (True; does; toWitness) +open import Relation.Nullary.Decidable.Core using (True; does; toWitness) open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl) open import Function.Base using (_$_) diff --git a/src/Data/Digit/Properties.agda b/src/Data/Digit/Properties.agda index 113bdde6ca..fb52d2af72 100644 --- a/src/Data/Digit/Properties.agda +++ b/src/Data/Digit/Properties.agda @@ -15,7 +15,7 @@ open import Data.Product.Base using (_,_; proj₁) open import Data.Vec.Relation.Unary.Unique.Propositional using (Unique) import Data.Vec.Relation.Unary.Unique.Propositional.Properties as Uniqueₚ open import Data.Vec.Relation.Unary.AllPairs using (allPairs?) -open import Relation.Nullary.Decidable using (True; from-yes; ¬?) +open import Relation.Nullary.Decidable.Core using (True; from-yes; ¬?) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) open import Function.Base using (_∘_) diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda index b0cf553d0d..1707fdc367 100644 --- a/src/Data/Fin/Induction.agda +++ b/src/Data/Fin/Induction.agda @@ -29,8 +29,8 @@ import Relation.Binary.Construct.NonStrictToStrict as ToStrict import Relation.Binary.Construct.On as On open import Relation.Binary.Definitions using (Tri; tri<; tri≈; tri>) open import Relation.Binary.PropositionalEquality -open import Relation.Nullary.Decidable using (yes; no) -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Decidable.Core using (yes; no) +open import Relation.Nullary.Negation.Core using (contradiction) open import Relation.Unary using (Pred) module Data.Fin.Induction where diff --git a/src/Data/Fin/Literals.agda b/src/Data/Fin/Literals.agda index 3fc30955ba..ae1c04ec57 100644 --- a/src/Data/Fin/Literals.agda +++ b/src/Data/Fin/Literals.agda @@ -9,12 +9,12 @@ module Data.Fin.Literals where open import Agda.Builtin.FromNat -open import Data.Nat using (suc; _≤?_) +open import Data.Nat using (_ Date: Mon, 14 Aug 2023 10:00:21 +0100 Subject: [PATCH 35/57] yet more simplified imports --- src/Algebra/Construct/LexProduct/Inner.agda | 4 ++-- src/Algebra/Properties/CancellativeCommutativeSemiring.agda | 4 ++-- src/Algebra/Solver/CommutativeMonoid.agda | 2 +- src/Algebra/Solver/IdempotentCommutativeMonoid.agda | 2 +- src/Algebra/Solver/Monoid.agda | 5 ++--- src/Algebra/Solver/Ring.agda | 2 +- src/Axiom/DoubleNegationElimination.agda | 2 +- src/Data/Fin/Subset/Properties.agda | 4 ++-- src/Data/Float/Properties.agda | 2 +- src/Data/List/Fresh/Relation/Unary/Any.agda | 4 ++-- src/Data/List/Relation/Unary/All/Properties.agda | 4 ++-- src/Data/Nat/Primality.agda | 2 +- 12 files changed, 18 insertions(+), 19 deletions(-) diff --git a/src/Algebra/Construct/LexProduct/Inner.agda b/src/Algebra/Construct/LexProduct/Inner.agda index 9b6e06f0e6..ac40a4299a 100644 --- a/src/Algebra/Construct/LexProduct/Inner.agda +++ b/src/Algebra/Construct/LexProduct/Inner.agda @@ -12,8 +12,8 @@ open import Data.Product.Base using (_×_; _,_; swap; map; uncurry′) open import Function.Base using (_∘_) open import Level using (Level; _⊔_) open import Relation.Binary.Definitions using (Decidable) -open import Relation.Nullary.Decidable using (does; yes; no) -open import Relation.Nullary.Negation +open import Relation.Nullary.Decidable.Core using (does; yes; no) +open import Relation.Nullary.Negation.Core using (contradiction; contradiction₂) import Relation.Binary.Reasoning.Setoid as SetoidReasoning diff --git a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda index e92fa5170e..25cfe832db 100644 --- a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda +++ b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda @@ -10,8 +10,8 @@ open import Algebra using (CancellativeCommutativeSemiring) open import Algebra.Definitions using (AlmostRightCancellative) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Relation.Binary.Definitions using (Decidable) -open import Relation.Nullary.Decidable using (yes; no) -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Decidable.Core using (yes; no) +open import Relation.Nullary.Negation.Core using (contradiction) module Algebra.Properties.CancellativeCommutativeSemiring {a ℓ} (R : CancellativeCommutativeSemiring a ℓ) diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda index 7e4b14b18c..ecca06739b 100644 --- a/src/Algebra/Solver/CommutativeMonoid.agda +++ b/src/Algebra/Solver/CommutativeMonoid.agda @@ -28,7 +28,7 @@ import Relation.Nullary.Decidable as Dec import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) -open import Relation.Nullary.Decidable using (Dec) +open import Relation.Nullary.Decidable.Core using (Dec) open CommutativeMonoid M open EqReasoning setoid diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda index fdba81a838..982f60bd32 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda @@ -26,7 +26,7 @@ import Relation.Nullary.Decidable as Dec import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise open import Relation.Binary.PropositionalEquality as P using (_≡_; decSetoid) -open import Relation.Nullary.Decidable using (Dec) +open import Relation.Nullary.Decidable.Core using (Dec) module Algebra.Solver.IdempotentCommutativeMonoid {m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda index f80a2847f6..2aa099a57a 100644 --- a/src/Algebra/Solver/Monoid.agda +++ b/src/Algebra/Solver/Monoid.agda @@ -24,8 +24,7 @@ open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) import Relation.Binary.Reflection -open import Relation.Nullary -import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Decidable.Core using (map′) open Monoid M open import Relation.Binary.Reasoning.Setoid setoid @@ -115,7 +114,7 @@ open module R = Relation.Binary.Reflection infix 5 _≟_ _≟_ : ∀ {n} → Decidable {A = Normal n} _≡_ -nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂) +nf₁ ≟ nf₂ = map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂) where open ListEq Fin._≟_ -- We can also give a sound, but not necessarily complete, procedure diff --git a/src/Algebra/Solver/Ring.agda b/src/Algebra/Solver/Ring.agda index 5bc696da38..ff40231a53 100644 --- a/src/Algebra/Solver/Ring.agda +++ b/src/Algebra/Solver/Ring.agda @@ -40,7 +40,7 @@ open _-Raw-AlmostCommutative⟶_ morphism renaming (⟦_⟧ to ⟦_⟧′) open import Algebra.Properties.Semiring.Exp semiring open import Relation.Binary -open import Relation.Nullary.Decidable using (yes; no) +open import Relation.Nullary.Decidable.Core using (yes; no) open import Relation.Binary.Reasoning.Setoid setoid import Relation.Binary.PropositionalEquality.Core as PropEq import Relation.Binary.Reflection as Reflection diff --git a/src/Axiom/DoubleNegationElimination.agda b/src/Axiom/DoubleNegationElimination.agda index 777f08c017..d427328c1e 100644 --- a/src/Axiom/DoubleNegationElimination.agda +++ b/src/Axiom/DoubleNegationElimination.agda @@ -12,7 +12,7 @@ open import Axiom.ExcludedMiddle open import Level open import Relation.Nullary open import Relation.Nullary.Negation -open import Relation.Nullary.Decidable +open import Relation.Nullary.Decidable.Core ------------------------------------------------------------------------ -- Definition diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda index 833f229c3a..a078a56b92 100644 --- a/src/Data/Fin/Subset/Properties.agda +++ b/src/Data/Fin/Subset/Properties.agda @@ -32,8 +32,8 @@ open import Function.Bundles using (_⇔_; mk⇔) open import Level using (Level) open import Relation.Binary as B hiding (Decidable; _⇔_) open import Relation.Binary.PropositionalEquality -open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎-dec_; map′) -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Decidable.Core using (Dec; yes; no; _⊎-dec_; map′) +open import Relation.Nullary.Negation.Core using (contradiction) open import Relation.Unary using (Pred; Decidable; Satisfiable) private diff --git a/src/Data/Float/Properties.agda b/src/Data/Float/Properties.agda index b2caebb616..25801d7cce 100644 --- a/src/Data/Float/Properties.agda +++ b/src/Data/Float/Properties.agda @@ -16,7 +16,7 @@ import Data.Nat.Properties as Nₚ import Data.Word.Base as Word import Data.Word.Properties as Wₚ open import Function.Base using (_∘_) -open import Relation.Nullary.Decidable as RN using (map′) +open import Relation.Nullary.Decidable.Core using (map′) open import Relation.Binary import Relation.Binary.Construct.On as On open import Relation.Binary.PropositionalEquality diff --git a/src/Data/List/Fresh/Relation/Unary/Any.agda b/src/Data/List/Fresh/Relation/Unary/Any.agda index 7a03010fae..c77154f040 100644 --- a/src/Data/List/Fresh/Relation/Unary/Any.agda +++ b/src/Data/List/Fresh/Relation/Unary/Any.agda @@ -14,7 +14,7 @@ open import Data.Product.Base using (∃; _,_; -,_) open import Data.Sum.Base using (_⊎_; [_,_]′; inj₁; inj₂) open import Function.Bundles using (_⇔_; mk⇔) open import Relation.Nullary.Negation.Core using (¬_) -open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎-dec_) +open import Relation.Nullary.Decidable.Core using (Dec; yes; no; _⊎-dec_; map′) open import Relation.Unary as U open import Relation.Binary.Core using (Rel) @@ -79,4 +79,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) = map′ fromSum toSum (P? x ⊎-dec any? xs) diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda index af41a14041..f99c7c3917 100644 --- a/src/Data/List/Relation/Unary/All/Properties.agda +++ b/src/Data/List/Relation/Unary/All/Properties.agda @@ -43,8 +43,8 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂; _≗_) open import Relation.Nullary open import Relation.Nullary.Reflects using (invert) -open import Relation.Nullary.Negation using (contradiction) -open import Relation.Nullary.Decidable using (¬?; decidable-stable) +open import Relation.Nullary.Negation.Core using (contradiction) +open import Relation.Nullary.Decidable.Core using (¬?; decidable-stable) open import Relation.Unary using (Decidable; Pred; Universal; ∁; _∩_; _⟨×⟩_) renaming (_⊆_ to _⋐_) open import Relation.Unary.Properties using (∁?) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 1473eb129c..74f083edef 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -16,7 +16,7 @@ open import Data.Nat.Properties open import Data.Product.Base using (∃; _×_; map₂; _,_) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Function.Base using (flip; _∘_; _∘′_) -open import Relation.Nullary.Decidable +open import Relation.Nullary.Decidable.Core using (yes; no; from-yes; map′; ¬?; decidable-stable; _×-dec_; _→-dec_) open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Unary using (Decidable) From 9db629ff6e05aeacacfc4ecdb5e28f9967a266f6 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 14 Aug 2023 10:36:22 +0100 Subject: [PATCH 36/57] yet more simplified imports --- src/Codata/Musical/Colist.agda | 3 +-- src/Codata/Sized/Cofin/Literals.agda | 2 +- src/Codata/Sized/Conat/Properties.agda | 2 +- src/Data/Fin/Properties.agda | 4 ++-- 4 files changed, 5 insertions(+), 6 deletions(-) diff --git a/src/Codata/Musical/Colist.agda b/src/Codata/Musical/Colist.agda index 3ef672abc7..a685a20fed 100644 --- a/src/Codata/Musical/Colist.agda +++ b/src/Codata/Musical/Colist.agda @@ -34,9 +34,8 @@ import Relation.Binary.Reasoning.Preorder as PreR import Relation.Binary.Reasoning.PartialOrder as POR open import Relation.Binary.PropositionalEquality as P using (_≡_) open import Relation.Nullary.Reflects using (invert) -open import Relation.Nullary open import Relation.Nullary.Negation -open import Relation.Nullary.Decidable using (¬¬-excluded-middle) +open import Relation.Nullary.Decidable.Core using (Dec; _because_; ¬¬-excluded-middle) open import Relation.Unary using (Pred) private diff --git a/src/Codata/Sized/Cofin/Literals.agda b/src/Codata/Sized/Cofin/Literals.agda index 0995ad4d23..898993d67c 100644 --- a/src/Codata/Sized/Cofin/Literals.agda +++ b/src/Codata/Sized/Cofin/Literals.agda @@ -13,7 +13,7 @@ open import Agda.Builtin.FromNat open import Codata.Sized.Conat open import Codata.Sized.Conat.Properties open import Codata.Sized.Cofin -open import Relation.Nullary.Decidable +open import Relation.Nullary.Decidable.Core using (True; toWitness) number : ∀ n → Number (Cofin n) number n = record diff --git a/src/Codata/Sized/Conat/Properties.agda b/src/Codata/Sized/Conat/Properties.agda index 43d5662a9a..e4586d7ee5 100644 --- a/src/Codata/Sized/Conat/Properties.agda +++ b/src/Codata/Sized/Conat/Properties.agda @@ -15,7 +15,7 @@ open import Codata.Sized.Conat open import Codata.Sized.Conat.Bisimilarity open import Function.Base using (_∋_) open import Relation.Nullary -open import Relation.Nullary.Decidable using (map′) +open import Relation.Nullary.Decidable.Core using (map′) open import Relation.Binary private diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 4a6c54b9bb..81aaaccd7d 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -40,7 +40,7 @@ open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_; module ≡-Reasoning) open import Relation.Nullary.Decidable.Core using (Dec; _because_; does; yes; no; _×-dec_; _⊎-dec_; map′) -open import Relation.Nullary.Decidable as Dec using (via-injection) +open import Relation.Nullary.Decidable using (via-injection) open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Nullary.Reflects using (invert) open import Relation.Unary as U @@ -937,7 +937,7 @@ decFinSubset {suc n} {P = P} {Q} Q? 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? = map′ [ ∃-here , ∃-there ] ∃-toSum (P? zero ⊎-dec 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) From 34152d30245d818f610289716cf87df490ca90f6 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 15 Aug 2023 15:02:45 +0100 Subject: [PATCH 37/57] missed this first time around --- src/Relation/Nullary/Decidable.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda index a91a02b80a..8eb0710a34 100644 --- a/src/Relation/Nullary/Decidable.agda +++ b/src/Relation/Nullary/Decidable.agda @@ -18,8 +18,8 @@ open import Function.Bundles using (Injection; module Injection; module Equivalence; _⇔_; _↔_; mk↔′) open import Relation.Binary.Bundles using (Setoid; module Setoid) open import Relation.Binary.Definitions using (Decidable) -open import Relation.Nullary -open import Relation.Nullary.Negation +open import Relation.Nullary using (Irrelevant) +open import Relation.Nullary.Negation.Core using (¬_) open import Relation.Nullary.Reflects using (invert) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong′) From 97f3c749ec3b7ac334f5381905fdcce285bad5b9 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 15 Aug 2023 15:06:20 +0100 Subject: [PATCH 38/57] missed this first time around --- src/Data/Sum.agda | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Data/Sum.agda b/src/Data/Sum.agda index 99cdbd3620..3bc5a1a8b3 100644 --- a/src/Data/Sum.agda +++ b/src/Data/Sum.agda @@ -16,7 +16,9 @@ open import Data.Maybe.Base using (Maybe; just; nothing) open import Function.Base open import Level open import Relation.Nullary.Reflects using (invert) -open import Relation.Nullary using (Dec; yes; no; _because_; ¬_) +open import Relation.Nullary.Decidable.Core using (Dec; yes; no; _because_) +open import Relation.Nullary.Negation.Core using (¬_) + private variable From fdf4f79fa715ed4102b356e1a43db9d234b3c754 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 16 Aug 2023 06:25:48 +0100 Subject: [PATCH 39/57] further `import` simplification --- src/Relation/Nullary/Reflects.agda | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda index 9e1168438e..4c24a964d7 100644 --- a/src/Relation/Nullary/Reflects.agda +++ b/src/Relation/Nullary/Reflects.agda @@ -11,13 +11,12 @@ module Relation.Nullary.Reflects where open import Agda.Builtin.Equality open import Data.Bool.Base -open import Data.Empty open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) open import Level using (Level) open import Function.Base using (id; _$_; _∘_; const) -open import Relation.Nullary.Negation.Core +open import Relation.Nullary.Negation.Core using (¬_; contradiction; _¬-⊎_) private variable @@ -84,7 +83,7 @@ _→-reflects_ : ∀ {a b} → Reflects P a → Reflects Q b → Reflects (P → Q) (not a ∨ b) ofʸ p →-reflects ofʸ q = ofʸ (const q) ofʸ p →-reflects ofⁿ ¬q = ofⁿ (¬q ∘ (_$ p)) -ofⁿ ¬p →-reflects _ = ofʸ (⊥-elim ∘ ¬p) +ofⁿ ¬p →-reflects _ = ofʸ (λ p → contradiction p ¬p) ------------------------------------------------------------------------ -- Other lemmas @@ -96,6 +95,6 @@ fromEquivalence {b = false} sound complete = ofⁿ complete -- `Reflects` is deterministic. det : ∀ {b b′} → Reflects P b → Reflects P b′ → b ≡ b′ det (ofʸ p) (ofʸ p′) = refl -det (ofʸ p) (ofⁿ ¬p′) = ⊥-elim (¬p′ p) -det (ofⁿ ¬p) (ofʸ p′) = ⊥-elim (¬p p′) +det (ofʸ p) (ofⁿ ¬p′) = contradiction p ¬p′ +det (ofⁿ ¬p) (ofʸ p′) = contradiction p′ ¬p det (ofⁿ ¬p) (ofⁿ ¬p′) = refl From 44d163bd1dbfc135f212be2a0b737519fa16ed6a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 16 Aug 2023 06:45:11 +0100 Subject: [PATCH 40/57] =?UTF-8?q?further=20`import`=20simplification;=20ma?= =?UTF-8?q?de=20`True-=E2=86=94`=20less=20strict?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Relation/Nullary/Decidable.agda | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda index 8eb0710a34..e28149c2f1 100644 --- a/src/Relation/Nullary/Decidable.agda +++ b/src/Relation/Nullary/Decidable.agda @@ -9,8 +9,7 @@ module Relation.Nullary.Decidable where open import Level using (Level) -open import Data.Bool.Base using (true; false; if_then_else_) -open import Data.Empty using (⊥-elim) +open import Data.Bool.Base using (true; false) open import Data.Product.Base as Prod hiding (map) open import Data.Sum.Base as Sum hiding (map) open import Function.Base @@ -19,7 +18,7 @@ open import Function.Bundles using open import Relation.Binary.Bundles using (Setoid; module Setoid) open import Relation.Binary.Definitions using (Decidable) open import Relation.Nullary using (Irrelevant) -open import Relation.Nullary.Negation.Core using (¬_) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Nullary.Reflects using (invert) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong′) @@ -60,8 +59,10 @@ module _ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} -- A lemma relating True and Dec True-↔ : (dec : Dec P) → Irrelevant P → True dec ↔ P -True-↔ (yes p) irr = mk↔′ (λ _ → p) _ (irr p) cong′ -True-↔ (no ¬p) _ = mk↔′ (λ ()) ¬p (⊥-elim ∘ ¬p) λ () +True-↔ (true because [p]) irr = let p = invert [p] in + mk↔′ (λ _ → p) _ (irr p) cong′ +True-↔ (false because [¬p]) _ = let ¬p = invert [¬p] in + mk↔′ (λ ()) ¬p (λ p → contradiction p ¬p) λ () ------------------------------------------------------------------------ -- Result of decidability @@ -72,11 +73,11 @@ isYes≗does (false because _) = refl dec-true : (p? : Dec P) → P → does p? ≡ true dec-true (true because _ ) p = refl -dec-true (false because [¬p]) p = ⊥-elim (invert [¬p] p) +dec-true (false because [¬p]) p = contradiction p (invert [¬p]) dec-false : (p? : Dec P) → ¬ P → does p? ≡ false dec-false (false because _ ) ¬p = refl -dec-false (true because [p]) ¬p = ⊥-elim (¬p (invert [p])) +dec-false (true because [p]) ¬p = contradiction (invert [p]) ¬p dec-yes : (p? : Dec P) → P → ∃ λ p′ → p? ≡ yes p′ dec-yes p? p with dec-true p? p @@ -87,5 +88,4 @@ dec-no p? ¬p with dec-false p? ¬p dec-no (no _) _ | refl = refl dec-yes-irr : (p? : Dec P) → Irrelevant P → (p : P) → p? ≡ yes p -dec-yes-irr p? irr p with dec-yes p? p -... | p′ , eq rewrite irr p p′ = eq +dec-yes-irr p? irr p with p′ , eq ← dec-yes p? p rewrite irr p p′ = eq From 246683c2970d93f76473f6fc39e417aa02f9bfa0 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 16 Aug 2023 07:21:00 +0100 Subject: [PATCH 41/57] =?UTF-8?q?further=20`import`=20simplification;=20ma?= =?UTF-8?q?de=20`True=E2=86=94`=20less=20strict?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Function/Related/TypeIsomorphisms.agda | 23 +++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda index 775502e16c..8bbf0d3854 100644 --- a/src/Function/Related/TypeIsomorphisms.agda +++ b/src/Function/Related/TypeIsomorphisms.agda @@ -13,8 +13,7 @@ open import Algebra open import Algebra.Structures.Biased using (isCommutativeSemiringˡ) open import Axiom.Extensionality.Propositional using (Extensionality) open import Data.Bool.Base using (true; false) -open import Data.Empty using (⊥-elim) -open import Data.Empty.Polymorphic using (⊥) renaming (⊥-elim to ⊥ₚ-elim) +open import Data.Empty.Polymorphic using (⊥; ⊥-elim) open import Data.Product.Base as Prod using (_×_; Σ; curry; uncurry; _,_; -,_; <_,_>; proj₁; proj₂; ∃₂; ∃) open import Data.Product.Function.NonDependent.Propositional @@ -28,11 +27,13 @@ open import Function.Equality using (_⟨$⟩_) open import Function.Equivalence as Eq using (_⇔_; Equivalence) open import Function.Inverse as Inv using (_↔_; Inverse; inverse) open import Function.Related -open import Relation.Binary hiding (_⇔_) +open import Relation.Binary hiding (_⇔_; Irrelevant) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) -open import Relation.Nullary.Decidable.Core using (Dec; yes; no; True) +open import Relation.Nullary using (Irrelevant) +open import Relation.Nullary.Decidable.Core using (Dec; _because_; True) +open import Relation.Nullary.Reflects using (invert) import Relation.Nullary.Indexed as I -open import Relation.Nullary.Negation.Core using (¬_) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) ------------------------------------------------------------------------ -- Properties of Σ and _×_ @@ -64,10 +65,10 @@ open import Relation.Nullary.Negation.Core using (¬_) -- × has ⊥ has its zero ×-zeroˡ : ∀ ℓ → LeftZero _↔_ (⊥ {ℓ}) _×_ -×-zeroˡ ℓ A = inverse proj₁ < id , ⊥ₚ-elim > (λ { () }) (λ _ → P.refl) +×-zeroˡ ℓ A = inverse proj₁ < id , ⊥-elim > (λ { () }) (λ _ → P.refl) ×-zeroʳ : ∀ ℓ → RightZero _↔_ (⊥ {ℓ}) _×_ -×-zeroʳ ℓ A = inverse proj₂ < ⊥ₚ-elim , id > (λ { () }) λ _ → P.refl +×-zeroʳ ℓ A = inverse proj₂ < ⊥-elim , id > (λ { () }) λ _ → P.refl ×-zero : ∀ ℓ → Zero _↔_ ⊥ _×_ ×-zero ℓ = ×-zeroˡ ℓ , ×-zeroʳ ℓ @@ -330,11 +331,11 @@ Related-cong {A = A} {B} {C} {D} A≈B C≈D = -- A lemma relating True dec and P, where dec : Dec P True↔ : ∀ {p} {P : Set p} - (dec : Dec P) → ((p₁ p₂ : P) → p₁ ≡ p₂) → True dec ↔ P -True↔ (yes p) irr = + (dec : Dec P) → Irrelevant P → True dec ↔ P +True↔ (true because [p]) irr = let p = invert [p] in inverse (λ _ → p) (λ _ → _) (λ _ → P.refl) (irr _) -True↔ (no ¬p) _ = - inverse (λ()) ¬p (λ ()) (⊥-elim ∘ ¬p) +True↔ (false because [¬p]) _ = let ¬p = invert [¬p] in + inverse (λ()) ¬p (λ ()) (λ p → contradiction p ¬p) ------------------------------------------------------------------------ -- Equality between pairs can be expressed as a pair of equalities From 6de49ff7867c9e8c61c6902e4d6272773a3b5f25 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 16 Aug 2023 07:22:47 +0100 Subject: [PATCH 42/57] further `import` simplification --- src/Function/Related/TypeIsomorphisms.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda index 8bbf0d3854..ec38859338 100644 --- a/src/Function/Related/TypeIsomorphisms.agda +++ b/src/Function/Related/TypeIsomorphisms.agda @@ -32,7 +32,6 @@ open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) open import Relation.Nullary using (Irrelevant) open import Relation.Nullary.Decidable.Core using (Dec; _because_; True) open import Relation.Nullary.Reflects using (invert) -import Relation.Nullary.Indexed as I open import Relation.Nullary.Negation.Core using (¬_; contradiction) ------------------------------------------------------------------------ From 165e61f98f89a5bf60391537fabbb6cea2a1637b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 17 Aug 2023 15:03:36 +0100 Subject: [PATCH 43/57] tightened `import`s --- src/Data/List/Membership/Setoid.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda index 047620041d..72095bd9d0 100644 --- a/src/Data/List/Membership/Setoid.agda +++ b/src/Data/List/Membership/Setoid.agda @@ -11,12 +11,12 @@ open import Relation.Binary module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where open import Function.Base using (_∘_; id; flip) -open import Data.List.Base as List using (List; []; _∷_; length; lookup) +open import Data.List.Base as List using (List; []; _∷_) open import Data.List.Relation.Unary.Any using (Any; index; map; here; there) open import Data.Product.Base as Prod using (∃; _×_; _,_) open import Relation.Unary using (Pred) -open import Relation.Nullary.Negation using (¬_) +open import Relation.Nullary.Negation.Core using (¬_) open Setoid S renaming (Carrier to A) From 5c5e3bc9b005d9d1146f6bf2359ffea97385d89a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 18 Aug 2023 10:47:37 +0100 Subject: [PATCH 44/57] another round of import tightening --- src/Relation/Nullary/Decidable/Core.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda index eb0267da07..25479f6152 100644 --- a/src/Relation/Nullary/Decidable/Core.agda +++ b/src/Relation/Nullary/Decidable/Core.agda @@ -14,7 +14,6 @@ module Relation.Nullary.Decidable.Core where open import Level using (Level; Lift) open import Data.Bool.Base using (Bool; false; true; not; T; _∧_; _∨_) open import Data.Unit.Base using (⊤) -open import Data.Empty using (⊥) open import Data.Empty.Irrelevant using (⊥-elim) open import Data.Product.Base using (_×_) open import Data.Sum.Base using (_⊎_) @@ -177,7 +176,7 @@ proof (map′ P→Q Q→P (false because [¬p])) = ofⁿ (invert [¬p] ∘ Q→P decidable-stable : Dec P → Stable P decidable-stable (yes p) ¬¬p = p -decidable-stable (no ¬p) ¬¬p = ⊥-elim (¬¬p ¬p) +decidable-stable (no ¬p) ¬¬p = contradiction ¬p ¬¬p ¬-drop-Dec : Dec (¬ ¬ P) → Dec (¬ P) ¬-drop-Dec ¬¬p? = map′ negated-stable contradiction (¬? ¬¬p?) From 24296c85b8a97c1d27d36b829dcab5868e887966 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 18 Aug 2023 10:49:12 +0100 Subject: [PATCH 45/57] `Data.Bool` import tightening --- src/Data/Bool.agda | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/Data/Bool.agda b/src/Data/Bool.agda index 5fdbcc45e0..55ed146e2c 100644 --- a/src/Data/Bool.agda +++ b/src/Data/Bool.agda @@ -8,10 +8,6 @@ module Data.Bool where -open import Relation.Nullary -open import Relation.Binary -open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) - ------------------------------------------------------------------------ -- The boolean type and some operations From c405c122af1207d4d30008b1533f0ded5a7975d1 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 18 Aug 2023 11:12:52 +0100 Subject: [PATCH 46/57] reverted to lazier `decToMaybe` --- src/Data/Maybe/Base.agda | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Data/Maybe/Base.agda b/src/Data/Maybe/Base.agda index 08f843867e..378a252819 100644 --- a/src/Data/Maybe/Base.agda +++ b/src/Data/Maybe/Base.agda @@ -16,7 +16,8 @@ open import Data.Unit.Base using (⊤) open import Data.These.Base using (These; this; that; these) open import Data.Product.Base as Prod using (_×_; _,_) open import Function.Base -open import Relation.Nullary.Decidable.Core using (Dec; yes; no) +open import Relation.Nullary.Decidable.Core using (Dec; _because_) +open import Relation.Nullary.Reflects using (invert) private variable @@ -46,8 +47,8 @@ is-nothing : Maybe A → Bool is-nothing = not ∘ is-just decToMaybe : Dec A → Maybe A -decToMaybe (yes a) = just a -decToMaybe (no _) = nothing +decToMaybe (true because [a]) = just (invert [a]) +decToMaybe (false because _) = nothing -- A dependent eliminator. From d2e3ff9dcf7394d828bdafb5ff0b2ac9545e1db4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 18 Aug 2023 16:32:06 +0100 Subject: [PATCH 47/57] =?UTF-8?q?reverted=20to=20lazier=20`filter=E2=81=BA?= =?UTF-8?q?`=20and=20`derun=E2=81=BA-aux`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/List/Relation/Unary/Any/Properties.agda | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda index e91df749a6..5ab27f9f8c 100644 --- a/src/Data/List/Relation/Unary/Any/Properties.agda +++ b/src/Data/List/Relation/Unary/Any/Properties.agda @@ -45,8 +45,9 @@ open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl) open import Relation.Unary as U using (Pred; _⟨×⟩_; _⟨→⟩_) renaming (_⊆_ to _⋐_) -open import Relation.Nullary.Decidable.Core using (does; yes; no; ¬?; decidable-stable) +open import Relation.Nullary.Decidable.Core using (does; _because_; yes; no; ¬?; decidable-stable) open import Relation.Nullary.Negation.Core using (¬_; contradiction) +open import Relation.Nullary.Reflects using (invert) private open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ}) @@ -526,8 +527,8 @@ module _ (Q? : U.Decidable Q) where filter⁺ : (p : Any P xs) → Any P (filter Q? xs) ⊎ ¬ Q (Any.lookup p) filter⁺ {xs = x ∷ _} (here px) with Q? x - ... | yes _ = inj₁ (here px) - ... | no ¬Qx = inj₂ ¬Qx + ... | true because _ = inj₁ (here px) + ... | false because [¬Qx] = inj₂ (invert [¬Qx]) filter⁺ {xs = x ∷ _} (there p) with does (Q? x) ... | true = Sum.map₁ there (filter⁺ p) ... | false = filter⁺ p @@ -547,8 +548,8 @@ module _ {R : A → A → Set r} (R? : B.Decidable R) where derun⁺-aux : ∀ x xs → P Respects R → P x → Any P (derun R? (x ∷ xs)) derun⁺-aux x [] resp Px = here Px derun⁺-aux x (y ∷ xs) resp Px with R? x y - ... | yes Rxy = derun⁺-aux y xs resp (resp Rxy Px) - ... | no _ = here Px + ... | true because [Rxy] = derun⁺-aux y xs resp (resp (invert [Rxy]) Px) + ... | false because _ = here Px derun⁺ : P Respects R → Any P xs → Any P (derun R? xs) derun⁺ {xs = x ∷ xs} resp (here px) = derun⁺-aux x xs resp px From 77c6969dedd3cc9b54da9d1fad0a8b21b9a74b8a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 20 Aug 2023 11:54:33 +0100 Subject: [PATCH 48/57] partial reversion of `d2c59778b2554271f51e10b086848f3a8dc899f7` --- README/Design/Decidability.agda | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/README/Design/Decidability.agda b/README/Design/Decidability.agda index 6fe452d416..e81e7e98ca 100644 --- a/README/Design/Decidability.agda +++ b/README/Design/Decidability.agda @@ -8,7 +8,7 @@ module README.Design.Decidability where -open import Data.Bool +open import Data.Bool.Base open import Data.List.Base using (List; []; _∷_) open import Data.List.Properties using (∷-injective) open import Data.Nat @@ -37,7 +37,8 @@ ex₁ : (n : ℕ) → Reflects (zero ≡ suc n) false ex₁ n = ofⁿ λ () ex₂ : (b : Bool) → Reflects (T b) b -ex₂ = T⁺ +ex₂ false = ofⁿ id +ex₂ true = ofʸ tt ------------------------------------------------------------------------ -- Dec @@ -50,7 +51,8 @@ open import Relation.Nullary.Decidable.Core -- proof : Reflects P does ex₃ : (b : Bool) → Dec (T b) -ex₃ = bool⁺ +does (ex₃ b) = b +proof (ex₃ b) = ex₂ b -- We also have pattern synonyms `yes` and `no`, allowing both fields to be -- given at once. From 6b0dcce265fa3eb9657f5b1e0e0dc3a6f6826945 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 20 Aug 2023 12:00:02 +0100 Subject: [PATCH 49/57] partial reversion of `eac8e01ef822db9cf0591f179c6bd619b9a0fc34`: renaming --- src/Relation/Nullary/Decidable/Core.agda | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda index 25479f6152..aee6ca9d8e 100644 --- a/src/Relation/Nullary/Decidable/Core.agda +++ b/src/Relation/Nullary/Decidable/Core.agda @@ -52,13 +52,10 @@ pattern yes p = true because ofʸ p pattern no ¬p = false because ofⁿ ¬p ------------------------------------------------------------------------ --- decision procedures are Decidable +-- Booleans (decision procedures) are Decidable -bool⁺ : ∀ b → Dec (T b) -bool⁺ b = b because (T⁺ b) - -predᵇ⁺ : ∀ {a} {A : Set a} (p : A → Bool) (x : A) → Dec (T (p x)) -predᵇ⁺ p x = bool⁺ (p x) +T? : ∀ b → Dec (T b) +T? b = b because (T⁺ b) ------------------------------------------------------------------------ -- Recompute From 94c01f64f87601e62c808ac3c9bc837c746452b3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 20 Aug 2023 12:03:15 +0100 Subject: [PATCH 50/57] partial reversion of `eac8e01ef822db9cf0591f179c6bd619b9a0fc34`: `CHANGELOG` --- CHANGELOG.md | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index d58c8aba3f..222aa52b7c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2793,11 +2793,9 @@ Other minor changes subst₂-removable : subst₂ _∼_ eq₁ eq₂ p ≅ p ``` -* Added new constructors for `Relation.Nullary.Decidable` +* Added new constructor for `Relation.Nullary.Decidable` ``` - bool⁺ : ∀ b → Dec (T b) - predᵇ⁺ : (p : A → Bool) (x : A) → Dec (T (p x)) - + T? : ∀ b → Dec (T b) ``` * Added new constructor for `Relation.Nullary.Reflects` From 15f00052961e7c007c4b4061f0fa6629090a6c42 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 20 Aug 2023 12:06:14 +0100 Subject: [PATCH 51/57] tweak `CHANGELOG` --- CHANGELOG.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 222aa52b7c..de48f83f20 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2312,8 +2312,8 @@ Other minor changes _!≢0 : NonZero (n !) _!*_!≢0 : NonZero (m ! * n !) - anyUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∃ λ n → n < v × P n) - allUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∀ {n} → n < v → P n) + anyUpTo? : ∀ (P? : Decidable P) (v : ℕ) → Dec (∃ λ n → n < v × P n) + allUpTo? : ∀ (P? : Decidable P) (v : ℕ) → Dec (∀ {n} → n < v → P n) n≤1⇒n≡0∨n≡1 : n ≤ 1 → n ≡ 0 ⊎ n ≡ 1 From 3458900e4d8794c00370a432f27df59de549d013 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 20 Aug 2023 12:17:41 +0100 Subject: [PATCH 52/57] knock-on chnages; further simplified `import`s --- src/Data/Bool/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda index 31e683c5cd..91aa7de191 100644 --- a/src/Data/Bool/Properties.agda +++ b/src/Data/Bool/Properties.agda @@ -24,7 +24,7 @@ open import Level using (Level; 0ℓ) open import Relation.Binary hiding (_⇔_) open import Relation.Binary.PropositionalEquality.Core open import Relation.Binary.PropositionalEquality.Properties -open import Relation.Nullary.Decidable.Core using (True; does; proof; yes; no; bool⁺) +open import Relation.Nullary.Decidable.Core as Dec using (True; yes; no) import Relation.Unary as U open import Algebra.Definitions {A = Bool} _≡_ @@ -754,7 +754,7 @@ T-irrelevant : U.Irrelevant T T-irrelevant {true} _ _ = refl T? : U.Decidable T -T? = bool⁺ +T? = Dec.T? T?-diag : ∀ b → T b → True (T? b) T?-diag true _ = _ From c4f3b1f036b7b16ffcc0b2f2e4195991502e186c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 20 Aug 2023 12:33:07 +0100 Subject: [PATCH 53/57] merge conflict resolution --- src/Algebra/Solver/Ring.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Algebra/Solver/Ring.agda b/src/Algebra/Solver/Ring.agda index ff40231a53..fe18b8e9e6 100644 --- a/src/Algebra/Solver/Ring.agda +++ b/src/Algebra/Solver/Ring.agda @@ -39,7 +39,6 @@ open import Algebra.Morphism open _-Raw-AlmostCommutative⟶_ morphism renaming (⟦_⟧ to ⟦_⟧′) open import Algebra.Properties.Semiring.Exp semiring -open import Relation.Binary open import Relation.Nullary.Decidable.Core using (yes; no) open import Relation.Binary.Reasoning.Setoid setoid import Relation.Binary.PropositionalEquality.Core as PropEq From 88e9e55bab03c317e27b3ae7cce7b8573a30ae79 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 20 Aug 2023 12:45:54 +0100 Subject: [PATCH 54/57] merge conflict resolution --- .../Binary/Suffix/Heterogeneous/Properties.agda | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda index e3e1b2771c..fff82f0bb5 100644 --- a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda @@ -20,13 +20,15 @@ open import Data.List.Relation.Binary.Prefix.Heterogeneous as Prefix open import Data.Nat.Base open import Data.Nat.Properties open import Function.Base using (_$_; flip) +open import Relation.Binary.Core + using (REL; Rel; _⇒_) +open import Relation.Binary.Definitions as B + using (Trans; Antisym; Irrelevant) +open import Relation.Binary.PropositionalEquality.Core as P + using (_≡_; _≢_; refl; sym; subst; subst₂) open import Relation.Nullary.Decidable.Core using (does; map′) open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Unary as U using (Pred) -open import Relation.Binary as B - using (REL; Rel; Trans; Antisym; Irrelevant; _⇒_) -open import Relation.Binary.PropositionalEquality.Core as P - using (_≡_; _≢_; refl; sym; subst; subst₂) import Data.List.Properties as Listₚ import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties as Prefixₚ From 124da89b2d3a5b6df4b64de69cc595b1cdc208fb Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 28 Sep 2023 12:52:04 +0100 Subject: [PATCH 55/57] updated to reflect recent changes to `master` --- src/Relation/Nullary/Decidable.agda | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda index 352b390766..eefa08c532 100644 --- a/src/Relation/Nullary/Decidable.agda +++ b/src/Relation/Nullary/Decidable.agda @@ -10,6 +10,7 @@ module Relation.Nullary.Decidable where open import Level using (Level) open import Data.Bool.Base using (true; false) +open import Data.Empty using (⊥-elim) open import Data.Product.Base as Prod hiding (map) open import Data.Sum.Base as Sum hiding (map) open import Function.Base @@ -60,7 +61,7 @@ module _ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} True-↔ : (dec : Dec P) → Irrelevant P → True dec ↔ P True-↔ (true because [p]) irr = mk↔ₛ′ (λ _ → invert [p]) _ (irr (invert [p])) cong′ -True-↔ (false because ofⁿ ¬p) _ = mk↔ₛ′ (λ ()) (invert (ofⁿ ¬p)) (⊥-elim ∘ ¬p) λ () +True-↔ (false because [¬p]) irr = mk↔ₛ′ (λ ()) (invert [¬p]) (⊥-elim ∘ (invert [¬p])) λ () ------------------------------------------------------------------------ -- Result of decidability From cef8c2193c0ac7c627d581ac5632f6501694d949 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 28 Sep 2023 12:53:42 +0100 Subject: [PATCH 56/57] updated to reflect recent changes to `master` --- src/Data/Fin/Base.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index 349374f2b6..0f16a3a752 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -20,6 +20,7 @@ open import Level using (0ℓ) open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong) open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel) +open import Relation.Nullary.Negation.Core using (contradiction) private variable From f938d1bb6b7e578f66ab9688a2fc564cf6b8f90d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 28 Sep 2023 13:17:20 +0100 Subject: [PATCH 57/57] updated to reflect recent changes to `master` --- src/Data/Sum/Relation/Binary/Pointwise.agda | 5 +++-- src/Function/Related/TypeIsomorphisms.agda | 19 ++++++++----------- 2 files changed, 11 insertions(+), 13 deletions(-) diff --git a/src/Data/Sum/Relation/Binary/Pointwise.agda b/src/Data/Sum/Relation/Binary/Pointwise.agda index 05ce26c64d..5db8eefcfe 100644 --- a/src/Data/Sum/Relation/Binary/Pointwise.agda +++ b/src/Data/Sum/Relation/Binary/Pointwise.agda @@ -19,6 +19,7 @@ open import Relation.Binary open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) import Relation.Binary.PropositionalEquality.Properties as P + private variable a b c d ℓ₁ ℓ₂ ℓ₃ ℓ : Level @@ -77,8 +78,8 @@ drop-inj₂ (inj₂ x) = x ⊎-substitutive subst₁ subst₂ P (inj₁ x) = subst₁ (P ∘ inj₁) x ⊎-substitutive subst₁ subst₂ P (inj₂ x) = subst₂ (P ∘ inj₂) x -⊎-decidable : Decidable ∼₁ → Decidable ∼₂ → - Decidable (Pointwise ∼₁ ∼₂) +⊎-decidable : Decidable ≈₁ → Decidable ≈₂ → + Decidable (Pointwise ≈₁ ≈₂) ⊎-decidable _≟₁_ _≟₂_ (inj₁ x) (inj₁ y) = map′ inj₁ drop-inj₁ (x ≟₁ y) ⊎-decidable _≟₁_ _≟₂_ (inj₁ x) (inj₂ y) = no λ() ⊎-decidable _≟₁_ _≟₂_ (inj₂ x) (inj₁ y) = no λ() diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda index 7156612a57..7b810aba04 100644 --- a/src/Function/Related/TypeIsomorphisms.agda +++ b/src/Function/Related/TypeIsomorphisms.agda @@ -26,10 +26,11 @@ open import Function.Base open import Function.Bundles open import Function.Related.Propositional import Function.Construct.Identity as Identity -open import Relation.Binary hiding (_⇔_) +open import Relation.Binary hiding (_⇔_; Irrelevant) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) open import Relation.Nullary using (Irrelevant) open import Relation.Nullary.Decidable.Core using (Dec; _because_; True) +open import Relation.Nullary.Decidable using (True-↔) open import Relation.Nullary.Reflects using (invert) open import Relation.Nullary.Negation.Core using (¬_; contradiction) @@ -65,10 +66,10 @@ private -- × has ⊥ has its zero ×-zeroˡ : ∀ ℓ → LeftZero {ℓ = ℓ} _↔_ ⊥ _×_ -×-zeroˡ ℓ A = mk↔ₛ′ proj₁ < id , ⊥ₚ-elim > (λ _ → P.refl) (λ { () }) +×-zeroˡ ℓ A = mk↔ₛ′ proj₁ < id , ⊥-elim > (λ _ → P.refl) (λ { () }) ×-zeroʳ : ∀ ℓ → RightZero {ℓ = ℓ} _↔_ ⊥ _×_ -×-zeroʳ ℓ A = mk↔ₛ′ proj₂ < ⊥ₚ-elim , id > (λ _ → P.refl) (λ { () }) +×-zeroʳ ℓ A = mk↔ₛ′ proj₂ < ⊥-elim , id > (λ _ → P.refl) (λ { () }) ×-zero : ∀ ℓ → Zero _↔_ ⊥ _×_ ×-zero ℓ = ×-zeroˡ ℓ , ×-zeroʳ ℓ @@ -324,12 +325,8 @@ Related-cong {A = A} {B = B} {C = C} {D = D} A≈B C≈D = mk⇔ ------------------------------------------------------------------------ -- A lemma relating True dec and P, where dec : Dec P -True↔ : ∀ {p} {P : Set p} - (dec : Dec P) → ((p₁ p₂ : P) → p₁ ≡ p₂) → True dec ↔ P -True↔ ( true because [p]) irr = - mk↔ₛ′ (λ _ → invert [p]) (λ _ → _) (irr _) (λ _ → P.refl) -True↔ (false because ofⁿ ¬p) _ = - mk↔ₛ′ (λ()) (invert (ofⁿ ¬p)) (⊥-elim ∘ ¬p) (λ ()) +True↔ : (dec : Dec A) → Irrelevant A → True dec ↔ A +True↔ = True-↔ ------------------------------------------------------------------------ -- Equality between pairs can be expressed as a pair of equalities @@ -358,7 +355,7 @@ module _ {a b} {A : Set a} {B : A → Set b} {p₁ p₂ : Σ A B} where Σ-≡,≡↔≡ : (∃ λ (p : proj₁ p₁ ≡ proj₁ p₂) → P.subst B p (proj₂ p₁) ≡ proj₂ p₂) ↔ p₁ ≡ p₂ - Σ-≡,≡↔≡ = inverse Σ-≡,≡→≡ Σ-≡,≡←≡ left-inverse-of right-inverse-of + Σ-≡,≡↔≡ = mk↔ₛ′ Σ-≡,≡→≡ Σ-≡,≡←≡ right-inverse-of left-inverse-of module _ {a b} {A : Set a} {B : Set b} {p₁ p₂ : A × B} where ×-≡,≡→≡ : (proj₁ p₁ ≡ proj₁ p₂) × (proj₂ p₁ ≡ proj₂ p₂) → p₁ ≡ p₂ @@ -377,7 +374,7 @@ module _ {a b} {A : Set a} {B : Set b} {p₁ p₂ : A × B} where right-inverse-of P.refl = P.refl ×-≡,≡↔≡ : (proj₁ p₁ ≡ proj₁ p₂ × proj₂ p₁ ≡ proj₂ p₂) ↔ p₁ ≡ p₂ - ×-≡,≡↔≡ = inverse ×-≡,≡→≡ ×-≡,≡←≡ left-inverse-of right-inverse-of + ×-≡,≡↔≡ = mk↔ₛ′ ×-≡,≡→≡ ×-≡,≡←≡ right-inverse-of left-inverse-of ×-≡×≡↔≡,≡ : ∀ {a b} {A : Set a} {B : Set b} {x y} (p : A × B) → (x ≡ proj₁ p × y ≡ proj₂ p) ↔ (x , y) ≡ p