From bd2808fff4aad131befc86ce2119d3e4d3c1cbae Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Tue, 25 Oct 2022 11:51:37 +0900 Subject: [PATCH 1/3] Deprecate Relation.Nullary.(Sum/Product/Implication) --- CHANGELOG.md | 10 +++++ README/Design/Decidability.agda | 18 +++++---- src/Data/Fin/Properties.agda | 9 ++--- src/Data/Fin/Subset/Properties.agda | 4 +- src/Data/List/Fresh/Relation/Unary/All.agda | 4 +- src/Data/List/Fresh/Relation/Unary/Any.agda | 5 +-- src/Data/List/Properties.agda | 6 +-- .../Infix/Heterogeneous/Properties.agda | 6 +-- src/Data/List/Relation/Binary/Lex.agda | 7 ++-- src/Data/List/Relation/Binary/Pointwise.agda | 2 - .../Relation/Binary/Pointwise/Properties.agda | 3 +- .../Prefix/Heterogeneous/Properties.agda | 7 ++-- src/Data/List/Relation/Unary/All.agda | 1 - src/Data/List/Relation/Unary/AllPairs.agda | 4 +- src/Data/List/Relation/Unary/Any.agda | 3 +- src/Data/List/Relation/Unary/Grouped.agda | 33 +++++++++++----- src/Data/List/Relation/Unary/Linked.agda | 4 +- src/Data/Nat/Primality.agda | 11 +++--- src/Data/Product/Nary/NonDependent.agda | 3 +- src/Data/Product/Properties.agda | 4 +- .../Product/Relation/Binary/Lex/Strict.agda | 6 +-- .../Binary/Pointwise/NonDependent.agda | 3 +- src/Data/Rational/Properties.agda | 7 +--- src/Data/These/Properties.agda | 4 +- .../Tree/AVL/Indexed/Relation/Unary/All.agda | 4 +- .../Tree/AVL/Indexed/Relation/Unary/Any.agda | 4 +- src/Data/Vec/Functional/Properties.agda | 5 +-- src/Data/Vec/Properties.agda | 4 +- src/Data/Vec/Relation/Binary/Lex/Core.agda | 8 ++-- .../Relation/Binary/Pointwise/Inductive.agda | 4 +- 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 | 4 +- src/Reflection/AST/Abstraction.agda | 4 +- src/Reflection/AST/Argument.agda | 11 +++--- src/Reflection/AST/Argument/Information.agda | 4 +- src/Reflection/AST/Argument/Modality.agda | 7 ++-- src/Reflection/AST/Definition.agda | 3 +- src/Reflection/AST/Term.agda | 6 +-- .../Closure/Reflexive/Properties.agda | 4 +- .../Binary/Construct/Intersection.agda | 5 +-- .../Binary/Construct/NonStrictToStrict.agda | 5 +-- .../Binary/Construct/StrictToNonStrict.agda | 5 +-- src/Relation/Binary/Construct/Union.agda | 5 +-- src/Relation/Nary.agda | 5 +-- src/Relation/Nullary.agda | 17 +++++++-- src/Relation/Nullary/Decidable/Core.agda | 20 +++++++++- src/Relation/Nullary/Implication.agda | 31 +++------------ src/Relation/Nullary/Negation/Core.agda | 15 ++++++-- src/Relation/Nullary/Product.agda | 32 +++------------- src/Relation/Nullary/Reflects.agda | 36 +++++++++++++++--- src/Relation/Nullary/Sum.agda | 38 ++++--------------- src/Relation/Unary/Properties.agda | 5 +-- src/Text/Regex/Properties.agda | 11 +++--- 55 files changed, 215 insertions(+), 265 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 22732ed359..0cb1cd7cfa 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -534,6 +534,16 @@ Non-backwards compatible changes * Backwards compatibility has been maintained, as `Relation.Nullary` still re-exports these publicly. +* The modules: + ``` + Relation.Nullary.Product + Relation.Nullary.Sum + Relation.Nullary.Implication + ``` + have been deprecated and their contents moved to `Relation.Nullary.(Negation/Reflects/Decidable)` + however all their contents is re-exported by `Relation.Nullary` which is the easiest way to access + it now. + * In order to facilitate this reorganisation the following breaking moves have occured: - `¬?` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Decidable.Core` - `¬-reflects` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Reflects`. diff --git a/README/Design/Decidability.agda b/README/Design/Decidability.agda index 610f5d1352..fe4b0583cd 100644 --- a/README/Design/Decidability.agda +++ b/README/Design/Decidability.agda @@ -8,13 +8,6 @@ module README.Design.Decidability where --- Reflects and Dec are defined in Relation.Nullary, and operations on them can --- be found in Relation.Nullary.Reflects and Relation.Nullary.Decidable. - -open import Relation.Nullary as Nullary -open import Relation.Nullary.Reflects -open import Relation.Nullary.Decidable - open import Data.Bool open import Data.List open import Data.List.Properties using (∷-injective) @@ -25,7 +18,11 @@ open import Data.Unit open import Function open import Relation.Binary.PropositionalEquality open import Relation.Nary -open import Relation.Nullary.Product + +------------------------------------------------------------------------ +-- Reflects + +open import Relation.Nullary.Reflects infix 4 _≟₀_ _≟₁_ _≟₂_ @@ -43,6 +40,11 @@ ex₂ : (b : Bool) → Reflects (T b) b ex₂ false = ofⁿ id ex₂ true = ofʸ tt +------------------------------------------------------------------------ +-- Dec + +open import Relation.Nullary.Decidable + -- A proof of `Dec P` is a proof of `Reflects P b` for some `b`. -- `Dec P` is declared as a record, with fields: -- does : Bool diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 3698c066a3..031f24bff6 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -36,13 +36,10 @@ 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.Decidable as Dec using (map′) -open import Relation.Nullary.Reflects -open import Relation.Nullary.Negation using (contradiction) open import Relation.Nullary - using (Reflects; ofʸ; ofⁿ; Dec; _because_; does; proof; yes; no; ¬_) -open import Relation.Nullary.Product using (_×-dec_) -open import Relation.Nullary.Sum using (_⊎-dec_) + 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.Unary as U using (U; Pred; Decidable; _⊆_; Satisfiable; Universal) open import Relation.Unary.Properties using (U?) diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda index a2863f672a..f075e4ed81 100644 --- a/src/Data/Fin/Subset/Properties.agda +++ b/src/Data/Fin/Subset/Properties.agda @@ -32,10 +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 using (Dec; yes; no) -import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎-dec_) open import Relation.Nullary.Negation using (contradiction) -open import Relation.Nullary.Sum using (_⊎-dec_) open import Relation.Unary using (Pred; Decidable; Satisfiable) private diff --git a/src/Data/List/Fresh/Relation/Unary/All.agda b/src/Data/List/Fresh/Relation/Unary/All.agda index f44b28a291..22467bc508 100644 --- a/src/Data/List/Fresh/Relation/Unary/All.agda +++ b/src/Data/List/Fresh/Relation/Unary/All.agda @@ -11,9 +11,7 @@ module Data.List.Fresh.Relation.Unary.All where open import Level using (Level; _⊔_; Lift) open import Data.Product using (_×_; _,_; proj₁; uncurry) open import Data.Sum.Base as Sum using (inj₁; inj₂) -open import Relation.Nullary -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_) open import Relation.Unary as U open import Relation.Binary as B using (Rel) diff --git a/src/Data/List/Fresh/Relation/Unary/Any.agda b/src/Data/List/Fresh/Relation/Unary/Any.agda index 480d011006..fae8cbc919 100644 --- a/src/Data/List/Fresh/Relation/Unary/Any.agda +++ b/src/Data/List/Fresh/Relation/Unary/Any.agda @@ -13,9 +13,8 @@ open import Data.Empty open import Data.Product using (∃; _,_; -,_) open import Data.Sum.Base using (_⊎_; [_,_]′; inj₁; inj₂) open import Function.Bundles using (_⇔_; mk⇔) -open import Relation.Nullary -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Sum using (_⊎-dec_) +open import Relation.Nullary.Negation using (¬_) +open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎-dec_) open import Relation.Unary as U open import Relation.Binary as B using (Rel) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 5bc11aeef1..0e4e1b822d 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -36,10 +36,8 @@ import Relation.Binary.Reasoning.Setoid as EqR open import Relation.Binary.PropositionalEquality as P hiding ([_]) open import Relation.Binary as B using (Rel) open import Relation.Nullary.Reflects using (invert) -open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no) -open import Relation.Nullary.Negation using (contradiction) -open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋; ¬?) -open import Relation.Nullary.Product using (_×-dec_) +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 (∁?) diff --git a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda index 48ebe35237..a6e74c18a6 100644 --- a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda @@ -17,10 +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 using (¬_; yes; no; does) -open import Relation.Nullary.Decidable using (map′) -open import Relation.Nullary.Negation using (contradiction) -open import Relation.Nullary.Sum using (_⊎-dec_) +open import Relation.Nullary.Decidable using (yes; no; does; map′; _⊎-dec_) +open import Relation.Nullary.Negation using (¬_; contradiction) open import Relation.Unary as U using (Pred) open import Relation.Binary using (REL; _⇒_; Decidable; Trans; Antisym) open import Relation.Binary.PropositionalEquality using (_≢_; refl; cong) diff --git a/src/Data/List/Relation/Binary/Lex.agda b/src/Data/List/Relation/Binary/Lex.agda index 419cc5d378..92a4c9168d 100644 --- a/src/Data/List/Relation/Binary/Lex.agda +++ b/src/Data/List/Relation/Binary/Lex.agda @@ -16,10 +16,9 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]) open import Function.Base using (_∘_; flip; id) open import Function.Bundles using (_⇔_; mk⇔) open import Level using (_⊔_) -open import Relation.Nullary using (Dec; yes; no; ¬_) -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Product using (_×-dec_) -open import Relation.Nullary.Sum using (_⊎-dec_) +open import Relation.Nullary.Negation using (¬_) +open import Relation.Nullary.Decidable as Dec + using (Dec; yes; no; _×-dec_; _⊎-dec_) open import Relation.Binary hiding (_⇔_) open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_; head; tail) diff --git a/src/Data/List/Relation/Binary/Pointwise.agda b/src/Data/List/Relation/Binary/Pointwise.agda index a0ec61758c..cfe9509757 100644 --- a/src/Data/List/Relation/Binary/Pointwise.agda +++ b/src/Data/List/Relation/Binary/Pointwise.agda @@ -23,9 +23,7 @@ open import Data.Nat.Base using (ℕ; zero; suc) open import Data.Nat.Properties open import Level open import Relation.Nullary hiding (Irrelevant) -open import Relation.Nullary.Negation.Core using (contradiction) import Relation.Nullary.Decidable as Dec using (map′) -open import Relation.Nullary.Product using (_×-dec_) open import Relation.Unary as U using (Pred) open import Relation.Binary renaming (Rel to Rel₂) open import Relation.Binary.PropositionalEquality as P using (_≡_) diff --git a/src/Data/List/Relation/Binary/Pointwise/Properties.agda b/src/Data/List/Relation/Binary/Pointwise/Properties.agda index c7f59fd1a6..28154f908d 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 as P -open import Relation.Nullary using (yes; no) -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary using (yes; no; _×-dec_) import Relation.Nullary.Decidable as Dec open import Data.List.Relation.Binary.Pointwise.Base diff --git a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda index cb3b66adc3..7f1c76a50d 100644 --- a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda @@ -20,11 +20,10 @@ open import Data.List.Relation.Binary.Prefix.Heterogeneous as Prefix hiding (Pre open import Data.Nat.Base using (ℕ; zero; suc; _≤_; z≤n; s≤s) open import Data.Nat.Properties using (suc-injective) open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂; uncurry) -open import Function +open import Function.Base -open import Relation.Nullary using (yes; no; ¬_; _because_) -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Negation using (¬_) +open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no; _because_) open import Relation.Unary as U using (Pred) open import Relation.Binary open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_) diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda index 33f71dcca5..a878d01dd3 100644 --- a/src/Data/List/Relation/Unary/All.agda +++ b/src/Data/List/Relation/Unary/All.agda @@ -22,7 +22,6 @@ open import Function open import Level open import Relation.Nullary hiding (Irrelevant) import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Product using (_×-dec_) open import Relation.Unary hiding (_∈_) open import Relation.Binary using (Setoid; _Respects_) open import Relation.Binary.PropositionalEquality as P diff --git a/src/Data/List/Relation/Unary/AllPairs.agda b/src/Data/List/Relation/Unary/AllPairs.agda index a320f03d73..c99767cc52 100644 --- a/src/Data/List/Relation/Unary/AllPairs.agda +++ b/src/Data/List/Relation/Unary/AllPairs.agda @@ -20,9 +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 using (yes; no) -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no) ------------------------------------------------------------------------ -- Definition diff --git a/src/Data/List/Relation/Unary/Any.agda b/src/Data/List/Relation/Unary/Any.agda index 02f7219229..f56e46dd6f 100644 --- a/src/Data/List/Relation/Unary/Any.agda +++ b/src/Data/List/Relation/Unary/Any.agda @@ -14,10 +14,9 @@ open import Data.List.Base as List using (List; []; [_]; _∷_) open import Data.Product 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) +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.Sum using (_⊎-dec_) open import Relation.Unary hiding (_∈_) private diff --git a/src/Data/List/Relation/Unary/Grouped.agda b/src/Data/List/Relation/Unary/Grouped.agda index eecdb1f75f..c1c9b75994 100644 --- a/src/Data/List/Relation/Unary/Grouped.agda +++ b/src/Data/List/Relation/Unary/Grouped.agda @@ -14,24 +14,37 @@ open import Data.Sum using (_⊎_; inj₁; inj₂) open import Data.Product using (_×_; _,_) open import Relation.Binary as B using (REL; Rel) open import Relation.Unary as U using (Pred) -open import Relation.Nullary using (¬_; yes) -open import Relation.Nullary.Decidable as Dec using (¬?) -open import Relation.Nullary.Sum using (_⊎-dec_) -open import Relation.Nullary.Product using (_×-dec_) -open import Level using (_⊔_) +open import Relation.Nullary.Negation using (¬_) +open import Relation.Nullary.Decidable as Dec using (yes; ¬?; _⊎-dec_; _×-dec_) +open import Level using (Level; _⊔_) + +private + variable + a ℓ : Level + A : Set a + x y : A + xs : List A + +------------------------------------------------------------------------ +-- Definition infixr 5 _∷≉_ _∷≈_ -data Grouped {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) : Pred (List A) (a ⊔ ℓ) where +data Grouped {A : Set a} (_≈_ : Rel A ℓ) : Pred (List A) (a ⊔ ℓ) where [] : Grouped _≈_ [] - _∷≉_ : ∀ {x xs} → All (λ y → ¬ (x ≈ y)) xs → Grouped _≈_ xs → Grouped _≈_ (x ∷ xs) - _∷≈_ : ∀ {x y xs} → x ≈ y → Grouped _≈_ (y ∷ xs) → Grouped _≈_ (x ∷ y ∷ xs) + _∷≉_ : All (λ y → ¬ (x ≈ y)) xs → Grouped _≈_ xs → Grouped _≈_ (x ∷ xs) + _∷≈_ : x ≈ y → Grouped _≈_ (y ∷ xs) → Grouped _≈_ (x ∷ y ∷ xs) + +------------------------------------------------------------------------ +-- Basic properties + +module _ {_≈_ : Rel A ℓ} where -module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} where grouped? : B.Decidable _≈_ → U.Decidable (Grouped _≈_) 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))) + grouped? _≟_ (x ∷ y ∷ xs) = + Dec.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 dca6c056dd..6a1440203c 100644 --- a/src/Data/List/Relation/Unary/Linked.agda +++ b/src/Data/List/Relation/Unary/Linked.agda @@ -20,9 +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 using (yes; no) -open import Relation.Nullary.Decidable as Dec using (map′) -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Decidable using (yes; no; map′; _×-dec_) private variable diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index e2d93fc61d..ac0b2d3585 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -16,13 +16,12 @@ open import Data.Nat.Properties open import Data.Product open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Function.Base using (flip; _∘_; _∘′_) -open import Relation.Nullary using (yes; no; ¬_) -open import Relation.Nullary.Decidable as Dec using (from-yes; ¬?; decidable-stable) -open import Relation.Nullary.Product using (_×-dec_) -open import Relation.Nullary.Implication using (_→-dec_) -open import Relation.Nullary.Negation using (contradiction) +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.Unary using (Decidable) -open import Relation.Binary.PropositionalEquality using (refl; sym; cong; subst) +open import Relation.Binary.PropositionalEquality + using (refl; sym; cong; subst) private variable diff --git a/src/Data/Product/Nary/NonDependent.agda b/src/Data/Product/Nary/NonDependent.agda index e5fc523109..de390a5f2a 100644 --- a/src/Data/Product/Nary/NonDependent.agda +++ b/src/Data/Product/Nary/NonDependent.agda @@ -22,8 +22,7 @@ open import Data.Sum.Base using (_⊎_) open import Data.Nat.Base using (ℕ; zero; suc; pred) open import Data.Fin.Base using (Fin; zero; suc) open import Function.Base using (const; _∘′_; _∘_) -open import Relation.Nullary -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Decidable using (Dec; yes; no; _×-dec_) open import Relation.Binary using (Rel) open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong₂) diff --git a/src/Data/Product/Properties.agda b/src/Data/Product/Properties.agda index 649c63715c..949667286b 100644 --- a/src/Data/Product/Properties.agda +++ b/src/Data/Product/Properties.agda @@ -14,9 +14,7 @@ open import Function open import Level using (Level) open import Relation.Binary using (DecidableEquality) open import Relation.Binary.PropositionalEquality -open import Relation.Nullary.Product -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary using (Dec; yes; no) +open import Relation.Nullary.Decidable as Dec using (Dec; yes; no) private variable diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda index 0dccfc4216..0958e45883 100644 --- a/src/Data/Product/Relation/Binary/Lex/Strict.agda +++ b/src/Data/Product/Relation/Binary/Lex/Strict.agda @@ -11,7 +11,7 @@ module Data.Product.Relation.Binary.Lex.Strict where -open import Data.Product +open import Data.Product.Base open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise using (Pointwise) open import Data.Sum.Base using (inj₁; inj₂; _-⊎-_; [_,_]) @@ -19,9 +19,7 @@ open import Data.Empty open import Function.Base open import Induction.WellFounded open import Level -open import Relation.Nullary -open import Relation.Nullary.Product -open import Relation.Nullary.Sum +open import Relation.Nullary.Decidable open import Relation.Binary open import Relation.Binary.Consequences open import Relation.Binary.PropositionalEquality using (_≡_; refl) diff --git a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda index e79933371f..56b6b37933 100644 --- a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda +++ b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda @@ -25,8 +25,7 @@ open import Function.LeftInverse as LeftInv open import Function.Related open import Function.Surjection as Surj using (Surjection; _↠_; module Surjection) -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Product +open import Relation.Nullary.Decidable using (_×-dec_) open import Relation.Binary open import Relation.Binary.PropositionalEquality as P using (_≡_) diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index 6826094088..3851b0601c 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -52,12 +52,9 @@ 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 using (¬_; yes; no; recompute) open import Relation.Nullary.Decidable as Dec - using (True; False; fromWitness; fromWitnessFalse; toWitnessFalse) -open import Relation.Nullary.Negation using (contradiction; contraposition) -open import Relation.Nullary.Decidable as Dec using (True; fromWitness; map′) -open import Relation.Nullary.Product using (_×-dec_) + using (True; False; fromWitness; fromWitnessFalse; toWitnessFalse; yes; no; recompute; map′; _×-dec_) +open import Relation.Nullary.Negation using (¬_; contradiction; contraposition) open import Algebra.Definitions {A = ℚ} _≡_ open import Algebra.Structures {A = ℚ} _≡_ diff --git a/src/Data/These/Properties.agda b/src/Data/These/Properties.agda index 98ed00e697..55672ed63f 100644 --- a/src/Data/These/Properties.agda +++ b/src/Data/These/Properties.agda @@ -13,9 +13,7 @@ open import Data.These.Base open import Function.Base using (_∘_) open import Relation.Binary using (Decidable) open import Relation.Binary.PropositionalEquality -open import Relation.Nullary using (yes; no) -open import Relation.Nullary.Decidable using (map′) -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Decidable using (yes; no; map′; _×-dec_) ------------------------------------------------------------------------ -- Equality diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda index 67baab339a..f2be362cb1 100644 --- a/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda +++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda @@ -21,9 +21,7 @@ open import Function.Nary.NonDependent using (congₙ) open import Level using (Level; _⊔_) open import Relation.Binary.PropositionalEquality using (_≡_; refl) -open import Relation.Nullary using (Dec; yes) -open import Relation.Nullary.Decidable using (map′) -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Decidable 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 5ff87e7c14..4f6978faf5 100644 --- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda +++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda @@ -18,9 +18,7 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) open import Function.Base using (_∘′_; _∘_) open import Level using (Level; _⊔_) -open import Relation.Nullary using (Dec; no) -open import Relation.Nullary.Decidable using (map′) -open import Relation.Nullary.Sum using (_⊎-dec_) +open import Relation.Nullary.Decidable using (Dec; no; map′; _⊎-dec_) open import Relation.Unary open StrictTotalOrder strictTotalOrder renaming (Carrier to Key) diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda index 926627ed17..311b62bd31 100644 --- a/src/Data/Vec/Functional/Properties.agda +++ b/src/Data/Vec/Functional/Properties.agda @@ -23,9 +23,8 @@ open import Function.Base open import Level using (Level) open import Relation.Binary as B open import Relation.Binary.PropositionalEquality -open import Relation.Nullary using (Dec; does; yes; no) -open import Relation.Nullary.Decidable using (map′) -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Decidable + using (Dec; does; yes; no; map′; _×-dec_) import Data.Fin.Properties as Finₚ diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 805570c42e..7f55bdc00c 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -27,9 +27,7 @@ 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 using (Dec; does; yes; no) -open import Relation.Nullary.Decidable using (map′) -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Decidable using (Dec; does; yes; no; _×-dec_; map′) open import Relation.Nullary.Negation 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 4a896b7aef..fdabddbf04 100644 --- a/src/Data/Vec/Relation/Binary/Lex/Core.agda +++ b/src/Data/Vec/Relation/Binary/Lex/Core.agda @@ -17,15 +17,13 @@ open import Data.Vec using (Vec; []; _∷_) open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _∷_) open import Function.Base using (flip) open import Function.Bundles using (_⇔_; mk⇔) +open import Level using (Level; _⊔_) open import Relation.Binary hiding (_⇔_) open import Relation.Binary.PropositionalEquality as P using (_≡_; refl; cong) -open import Relation.Nullary as Nullary hiding (Irrelevant) -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Product using (_×-dec_) -open import Relation.Nullary.Sum using (_⊎-dec_) +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 Level using (Level; _⊔_) private variable diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda index bac12f80c1..5f85d23894 100644 --- a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda +++ b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda @@ -18,9 +18,7 @@ open import Function.Base using (_∘_) open import Function.Bundles using (_⇔_; mk⇔) open import Relation.Binary open import Relation.Binary.PropositionalEquality as P using (_≡_) -open import Relation.Nullary -open import Relation.Nullary.Decidable using (map′) -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Decidable 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 b16340ef6b..d59686bdad 100644 --- a/src/Data/Vec/Relation/Unary/All.agda +++ b/src/Data/Vec/Relation/Unary/All.agda @@ -17,9 +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 hiding (Irrelevant) -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no) open import Relation.Unary hiding (_∈_) open import Relation.Binary using (Setoid; _Respects_) open import Relation.Binary.PropositionalEquality as P using (subst) diff --git a/src/Data/Vec/Relation/Unary/AllPairs.agda b/src/Data/Vec/Relation/Unary/AllPairs.agda index adf5af2c9d..58e500a9f0 100644 --- a/src/Data/Vec/Relation/Unary/AllPairs.agda +++ b/src/Data/Vec/Relation/Unary/AllPairs.agda @@ -21,9 +21,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 using (yes; no) -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Decidable as Dec using (yes; no; _×-dec_) ------------------------------------------------------------------------ -- Definition diff --git a/src/Data/Vec/Relation/Unary/Any.agda b/src/Data/Vec/Relation/Unary/Any.agda index a54991976f..f400e25f86 100644 --- a/src/Data/Vec/Relation/Unary/Any.agda +++ b/src/Data/Vec/Relation/Unary/Any.agda @@ -15,10 +15,8 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) open import Data.Vec.Base as Vec using (Vec; []; [_]; _∷_) open import Data.Product as Prod using (∃; _,_) open import Level using (Level; _⊔_) -open import Relation.Nullary using (¬_; yes; no) -open import Relation.Nullary.Negation using (contradiction) -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Sum using (_⊎-dec_) +open import Relation.Nullary.Negation using (¬_; contradiction) +open import Relation.Nullary.Decidable as Dec using (yes; no; _⊎-dec_) open import Relation.Unary private diff --git a/src/Data/Vec/Relation/Unary/Linked.agda b/src/Data/Vec/Relation/Unary/Linked.agda index 9183ac325d..641452fac1 100644 --- a/src/Data/Vec/Relation/Unary/Linked.agda +++ b/src/Data/Vec/Relation/Unary/Linked.agda @@ -18,9 +18,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 using (yes; no) -open import Relation.Nullary.Decidable as Dec using (map′) -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Decidable as Dec using (yes; no; _×-dec_; map′) private variable diff --git a/src/Reflection/AST/Abstraction.agda b/src/Reflection/AST/Abstraction.agda index 809533981f..bc7b6ba034 100644 --- a/src/Reflection/AST/Abstraction.agda +++ b/src/Reflection/AST/Abstraction.agda @@ -12,9 +12,7 @@ open import Data.List.Base as List using (List) open import Data.Product using (_×_; _,_; uncurry; <_,_>) open import Data.String as String using (String) open import Level -open import Relation.Nullary -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Decidable as Dec using (Dec; _×-dec_) open import Relation.Binary open import Relation.Binary.PropositionalEquality diff --git a/src/Reflection/AST/Argument.agda b/src/Reflection/AST/Argument.agda index 39a1b20ffa..0374f15102 100644 --- a/src/Reflection/AST/Argument.agda +++ b/src/Reflection/AST/Argument.agda @@ -11,17 +11,16 @@ module Reflection.AST.Argument where open import Data.List.Base as List using (List; []; _∷_) open import Data.Product using (_×_; _,_; uncurry; <_,_>) open import Data.Nat using (ℕ) +open import Relation.Nullary.Decidable as Dec using (Dec; _×-dec_) +open import Relation.Binary +open import Relation.Binary.PropositionalEquality +open import Level + open import Reflection.AST.Argument.Visibility open import Reflection.AST.Argument.Relevance open import Reflection.AST.Argument.Quantity open import Reflection.AST.Argument.Modality open import Reflection.AST.Argument.Information as Information -open import Relation.Nullary -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Product using (_×-dec_) -open import Relation.Binary -open import Relation.Binary.PropositionalEquality -open import Level private variable diff --git a/src/Reflection/AST/Argument/Information.agda b/src/Reflection/AST/Argument/Information.agda index 0ba3f53bea..7838f016bc 100644 --- a/src/Reflection/AST/Argument/Information.agda +++ b/src/Reflection/AST/Argument/Information.agda @@ -8,9 +8,9 @@ module Reflection.AST.Argument.Information where -open import Data.Product +open import Data.Product.Base import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary using (_×-dec_) open import Relation.Binary open import Relation.Binary.PropositionalEquality diff --git a/src/Reflection/AST/Argument/Modality.agda b/src/Reflection/AST/Argument/Modality.agda index ca8d9519f7..4fc97dbd99 100644 --- a/src/Reflection/AST/Argument/Modality.agda +++ b/src/Reflection/AST/Argument/Modality.agda @@ -8,10 +8,9 @@ module Reflection.AST.Argument.Modality where -open import Data.Product -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Product using (_×-dec_) -open import Relation.Binary +open import Data.Product.Base +open import Relation.Nullary.Decidable as Dec using (_×-dec_) +open import Relation.Binary using (DecidableEquality) open import Relation.Binary.PropositionalEquality open import Reflection.AST.Argument.Relevance as Relevance using (Relevance) diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda index 2825b5c474..65e71f368c 100644 --- a/src/Reflection/AST/Definition.agda +++ b/src/Reflection/AST/Definition.agda @@ -16,8 +16,7 @@ open import Data.Product using (_×_; <_,_>; uncurry) open import Data.String as String using (String; _<+>_; intersperse; braces) open import Function.Base using (_∘′_) open import Relation.Nullary -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no) open import Relation.Binary using (DecidableEquality) open import Relation.Binary.PropositionalEquality diff --git a/src/Reflection/AST/Term.agda b/src/Reflection/AST/Term.agda index ddb02b4afe..19b38f10e7 100644 --- a/src/Reflection/AST/Term.agda +++ b/src/Reflection/AST/Term.agda @@ -16,9 +16,7 @@ import Data.Product.Properties as Product open import Data.Maybe.Base using (Maybe; just; nothing) open import Data.String as String using (String) open import Function.Base using (_∘_) -open import Relation.Nullary -open import Relation.Nullary.Product using (_×-dec_) -open import Relation.Nullary.Decidable as Dec +open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no) open import Relation.Binary open import Relation.Binary.PropositionalEquality @@ -168,7 +166,7 @@ arg i a ≟-ArgType arg i′ a′ = unArg-dec (a ≟ a′) _≟-Telescope_ : DecidableEquality Telescope [] ≟-Telescope [] = yes refl ((x , t) ∷ tel) ≟-Telescope ((x′ , t′) ∷ tel′) = Lₚ.∷-dec - (map′ (uncurry (cong₂ _,_)) Product.,-injective ((x String.≟ x′) ×-dec (t ≟-ArgTerm t′))) + (Dec.map′ (uncurry (cong₂ _,_)) Product.,-injective ((x String.≟ x′) ×-dec (t ≟-ArgTerm t′))) (tel ≟-Telescope tel′) [] ≟-Telescope (_ ∷ _) = no λ () (_ ∷ _) ≟-Telescope [] = no λ () diff --git a/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda b/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda index e251196768..893e9126a4 100644 --- a/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda +++ b/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda @@ -8,7 +8,7 @@ module Relation.Binary.Construct.Closure.Reflexive.Properties where -open import Data.Product as Prod +open import Data.Product.Base as Prod open import Data.Sum.Base as Sum open import Function.Bundles using (_⇔_; mk⇔) open import Function.Base using (id) @@ -18,8 +18,6 @@ open import Relation.Binary.Construct.Closure.Reflexive open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl) open import Relation.Nullary import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Negation using (contradiction) -open import Relation.Nullary.Sum using (_⊎-dec_) open import Relation.Unary using (Pred) private diff --git a/src/Relation/Binary/Construct/Intersection.agda b/src/Relation/Binary/Construct/Intersection.agda index b65dbb0414..6f378a6ff1 100644 --- a/src/Relation/Binary/Construct/Intersection.agda +++ b/src/Relation/Binary/Construct/Intersection.agda @@ -8,13 +8,12 @@ module Relation.Binary.Construct.Intersection where -open import Data.Product +open import Data.Product.Base 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 using (yes; no) -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Decidable using (yes; no; _×-dec_) private variable diff --git a/src/Relation/Binary/Construct/NonStrictToStrict.agda b/src/Relation/Binary/Construct/NonStrictToStrict.agda index 8f1099b4a9..eed860f088 100644 --- a/src/Relation/Binary/Construct/NonStrictToStrict.agda +++ b/src/Relation/Binary/Construct/NonStrictToStrict.agda @@ -11,13 +11,12 @@ open import Relation.Binary module Relation.Binary.Construct.NonStrictToStrict {a ℓ₁ ℓ₂} {A : Set a} (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) where -open import Data.Product using (_×_; _,_; proj₁; proj₂) +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 (¬?) -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Decidable using (¬?; _×-dec_) private _≉_ : Rel A ℓ₁ diff --git a/src/Relation/Binary/Construct/StrictToNonStrict.agda b/src/Relation/Binary/Construct/StrictToNonStrict.agda index 05c2b65810..dd1b7980ce 100644 --- a/src/Relation/Binary/Construct/StrictToNonStrict.agda +++ b/src/Relation/Binary/Construct/StrictToNonStrict.agda @@ -17,13 +17,12 @@ module Relation.Binary.Construct.StrictToNonStrict (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂) where -open import Data.Product +open import Data.Product.Base open import Data.Sum.Base open import Data.Empty open import Function.Base open import Relation.Binary.Consequences -open import Relation.Nullary -open import Relation.Nullary.Sum using (_⊎-dec_) +open import Relation.Nullary.Decidable using (_⊎-dec_; yes; no) ------------------------------------------------------------------------ -- Conversion diff --git a/src/Relation/Binary/Construct/Union.agda b/src/Relation/Binary/Construct/Union.agda index f4975601f6..b98d7dfb98 100644 --- a/src/Relation/Binary/Construct/Union.agda +++ b/src/Relation/Binary/Construct/Union.agda @@ -8,13 +8,12 @@ module Relation.Binary.Construct.Union where -open import Data.Product +open import Data.Product.Base 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 using (yes; no) -open import Relation.Nullary.Sum using (_⊎-dec_) +open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_) private variable diff --git a/src/Relation/Nary.agda b/src/Relation/Nary.agda index d5c38df741..107e3772f6 100644 --- a/src/Relation/Nary.agda +++ b/src/Relation/Nary.agda @@ -24,9 +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 using (¬_; Dec; yes; no; _because_) -import Relation.Nullary.Decidable as Dec -open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Nullary.Negation using (¬_) +open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _because_; _×-dec_) import Relation.Unary as Unary open import Relation.Binary.PropositionalEquality using (_≡_; cong; subst) diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda index b4766227c6..4eb7cb0b20 100644 --- a/src/Relation/Nullary.agda +++ b/src/Relation/Nullary.agda @@ -15,9 +15,20 @@ open import Agda.Builtin.Equality ------------------------------------------------------------------------ -- Re-exports -open import Relation.Nullary.Negation.Core public using (¬_) -open import Relation.Nullary.Reflects public using (Reflects; ofʸ; ofⁿ) -open import Relation.Nullary.Decidable.Core public using (Dec; yes; no; does; proof; recompute; _because_) +open import Relation.Nullary.Negation.Core public using + ( ¬_; _¬-⊎_ + ; contradiction; contradiction₂; contraposition + ) + +open import Relation.Nullary.Reflects public using + ( Reflects; ofʸ; ofⁿ + ; _×-reflects_; _⊎-reflects_; _→-reflects_ + ) + +open import Relation.Nullary.Decidable.Core public using + ( Dec; does; proof; yes; no; _because_; recompute + ; ¬?; _×-dec_; _⊎-dec_; _→-dec_ + ) ------------------------------------------------------------------------ -- Irrelevant types diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda index 1dc26b171e..48724feb7f 100644 --- a/src/Relation/Nullary/Decidable/Core.agda +++ b/src/Relation/Nullary/Decidable/Core.agda @@ -12,11 +12,12 @@ 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.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 +open import Data.Product using (_×_) +open import Data.Sum.Base using (_⊎_) open import Function.Base using (_∘_; const; _$_; flip) open import Relation.Nullary.Reflects open import Relation.Nullary.Negation.Core @@ -63,10 +64,25 @@ recompute (no ¬p) x = ⊥-elim (¬p x) ------------------------------------------------------------------------ -- Interaction with negation, sum, product etc. +infixr 1 _⊎-dec_ +infixr 2 _×-dec_ _→-dec_ + ¬? : Dec P → Dec (¬ P) does (¬? p?) = not (does p?) proof (¬? p?) = ¬-reflects (proof p?) +_×-dec_ : Dec P → Dec Q → Dec (P × Q) +does (p? ×-dec q?) = does p? ∧ does q? +proof (p? ×-dec q?) = proof p? ×-reflects proof q? + +_⊎-dec_ : Dec P → Dec Q → Dec (P ⊎ Q) +does (p? ⊎-dec q?) = does p? ∨ does q? +proof (p? ⊎-dec q?) = proof p? ⊎-reflects proof q? + +_→-dec_ : Dec P → Dec Q → Dec (P → Q) +does (p? →-dec q?) = not (does p?) ∨ does q? +proof (p? →-dec q?) = proof p? →-reflects proof q? + ------------------------------------------------------------------------ -- Relationship with booleans diff --git a/src/Relation/Nullary/Implication.agda b/src/Relation/Nullary/Implication.agda index cdf257c78d..65ab98fe1d 100644 --- a/src/Relation/Nullary/Implication.agda +++ b/src/Relation/Nullary/Implication.agda @@ -8,29 +8,10 @@ module Relation.Nullary.Implication where -open import Data.Bool.Base -open import Data.Empty -open import Function.Base -open import Relation.Nullary -open import Level +{-# WARNING_ON_IMPORT +"Relation.Nullary.Implication was deprecated in v2.0. +Use `Relation.Nullary` instead." +#-} -private - variable - p q : Level - P : Set p - Q : Set q - ------------------------------------------------------------------------- --- Some properties which are preserved by _→_. - -infixr 2 _→-reflects_ _→-dec_ - -_→-reflects_ : ∀ {bp bq} → Reflects P bp → Reflects Q bq → - Reflects (P → Q) (not bp ∨ bq) -ofʸ p →-reflects ofʸ q = ofʸ (const q) -ofʸ p →-reflects ofⁿ ¬q = ofⁿ (¬q ∘ (_$ p)) -ofⁿ ¬p →-reflects _ = ofʸ (⊥-elim ∘ ¬p) - -_→-dec_ : Dec P → Dec Q → Dec (P → Q) -does (p? →-dec q?) = not (does p?) ∨ does q? -proof (p? →-dec q?) = proof p? →-reflects proof q? +open import Relation.Nullary.Decidable.Core public using (_→-dec_) +open import Relation.Nullary.Reflects public using (_→-reflects_) diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda index 3a245b79a9..520914def3 100644 --- a/src/Relation/Nullary/Negation/Core.agda +++ b/src/Relation/Nullary/Negation/Core.agda @@ -9,10 +9,10 @@ module Relation.Nullary.Negation.Core where open import Data.Bool.Base using (not) -open import Data.Empty hiding (⊥-elim) -open import Data.Empty.Irrelevant -open import Data.Product.Base -open import Data.Sum.Base using (_⊎_; inj₁; inj₂) +open import Data.Empty using (⊥) +open import Data.Empty.Irrelevant using (⊥-elim) +open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) +open import Data.Sum.Base using (_⊎_; [_,_]; inj₁; inj₂) open import Function.Base using (flip; _$_; _∘_; const) open import Level @@ -39,6 +39,13 @@ DoubleNegation P = ¬ ¬ P Stable : Set p → Set p Stable P = ¬ ¬ P → P +------------------------------------------------------------------------ +-- Relationship to product and sum + +infixr 1 _¬-⊎_ +_¬-⊎_ : ¬ P → ¬ Q → ¬ (P ⊎ Q) +_¬-⊎_ = [_,_] + ------------------------------------------------------------------------ -- Uses of negation diff --git a/src/Relation/Nullary/Product.agda b/src/Relation/Nullary/Product.agda index 8bdfc01588..ca2a52bdb6 100644 --- a/src/Relation/Nullary/Product.agda +++ b/src/Relation/Nullary/Product.agda @@ -8,30 +8,10 @@ module Relation.Nullary.Product where -open import Data.Bool.Base -open import Data.Product -open import Function.Base using (_∘_) -open import Level -open import Relation.Nullary.Reflects -open import Relation.Nullary +{-# WARNING_ON_IMPORT +"Relation.Nullary.Product was deprecated in v2.0. +Use `Relation.Nullary` instead." +#-} -private - variable - p q : Level - P : Set p - Q : Set q - ------------------------------------------------------------------------- --- Some properties which are preserved by _×_. - -infixr 2 _×-reflects_ _×-dec_ - -_×-reflects_ : ∀ {bp bq} → Reflects P bp → Reflects Q bq → - Reflects (P × Q) (bp ∧ bq) -ofʸ p ×-reflects ofʸ q = ofʸ (p , q) -ofʸ p ×-reflects ofⁿ ¬q = ofⁿ (¬q ∘ proj₂) -ofⁿ ¬p ×-reflects _ = ofⁿ (¬p ∘ proj₁) - -_×-dec_ : Dec P → Dec Q → Dec (P × Q) -does (p? ×-dec q?) = does p? ∧ does q? -proof (p? ×-dec q?) = proof p? ×-reflects proof q? +open import Relation.Nullary.Decidable.Core public using (_×-dec_) +open import Relation.Nullary.Reflects public using (_×-reflects_) diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda index 683d9924c6..c6fcaf6ea6 100644 --- a/src/Relation/Nullary/Reflects.agda +++ b/src/Relation/Nullary/Reflects.agda @@ -9,17 +9,20 @@ module Relation.Nullary.Reflects where open import Agda.Builtin.Equality + open import Data.Bool.Base open import Data.Empty -open import Level -open import Function.Base using (_$_) +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 Relation.Nullary.Negation.Core private variable - p : Level - P : Set p + p q : Level + P Q : Set p ------------------------------------------------------------------------ -- `Reflects` idiom. @@ -48,16 +51,37 @@ invert : ∀ {b} → Reflects P b → if b then P else ¬ P invert (ofʸ p) = p invert (ofⁿ ¬p) = ¬p - ------------------------------------------------------------------------ -- Interaction with negation, product, sums etc. -- If we can decide P, then we can decide its negation. - ¬-reflects : ∀ {b} → Reflects P b → Reflects (¬ P) (not b) ¬-reflects (ofʸ p) = ofⁿ (_$ p) ¬-reflects (ofⁿ ¬p) = ofʸ ¬p +-- If we can decide P and Q then we can decide their product +infixr 2 _×-reflects_ +_×-reflects_ : ∀ {a b} → Reflects P a → Reflects Q b → + Reflects (P × Q) (a ∧ b) +ofʸ p ×-reflects ofʸ q = ofʸ (p , q) +ofʸ p ×-reflects ofⁿ ¬q = ofⁿ (¬q ∘ proj₂) +ofⁿ ¬p ×-reflects _ = ofⁿ (¬p ∘ proj₁) + + +infixr 1 _⊎-reflects_ +_⊎-reflects_ : ∀ {a b} → Reflects P a → Reflects Q b → + Reflects (P ⊎ Q) (a ∨ b) +ofʸ p ⊎-reflects _ = ofʸ (inj₁ p) +ofⁿ ¬p ⊎-reflects ofʸ q = ofʸ (inj₂ q) +ofⁿ ¬p ⊎-reflects ofⁿ ¬q = ofⁿ (¬p ¬-⊎ ¬q) + +infixr 2 _→-reflects_ +_→-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) + ------------------------------------------------------------------------ -- Other lemmas diff --git a/src/Relation/Nullary/Sum.agda b/src/Relation/Nullary/Sum.agda index 2c025fe47f..6860b9a643 100644 --- a/src/Relation/Nullary/Sum.agda +++ b/src/Relation/Nullary/Sum.agda @@ -8,33 +8,11 @@ module Relation.Nullary.Sum where -open import Data.Bool.Base -open import Data.Sum.Base -open import Data.Empty -open import Level -open import Relation.Nullary.Reflects -open import Relation.Nullary - -private - variable - p q : Level - P : Set p - Q : Set q - ------------------------------------------------------------------------- --- Some properties which are preserved by _⊎_. - -infixr 1 _¬-⊎_ _⊎-reflects_ _⊎-dec_ - -_¬-⊎_ : ¬ P → ¬ Q → ¬ (P ⊎ Q) -_¬-⊎_ = [_,_] - -_⊎-reflects_ : ∀ {bp bq} → Reflects P bp → Reflects Q bq → - Reflects (P ⊎ Q) (bp ∨ bq) -ofʸ p ⊎-reflects _ = ofʸ (inj₁ p) -ofⁿ ¬p ⊎-reflects ofʸ q = ofʸ (inj₂ q) -ofⁿ ¬p ⊎-reflects ofⁿ ¬q = ofⁿ (¬p ¬-⊎ ¬q) - -_⊎-dec_ : Dec P → Dec Q → Dec (P ⊎ Q) -does (p? ⊎-dec q?) = does p? ∨ does q? -proof (p? ⊎-dec q?) = proof p? ⊎-reflects proof q? +{-# WARNING_ON_IMPORT +"Relation.Nullary.Sum was deprecated in v2.0. +Use `Relation.Nullary` instead." +#-} + +open import Relation.Nullary.Negation.Core public using (_¬-⊎_) +open import Relation.Nullary.Reflects public using (_⊎-reflects_) +open import Relation.Nullary.Decidable.Core public using (_⊎-dec_) diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda index 08a258b803..5cdbcb6015 100644 --- a/src/Relation/Unary/Properties.agda +++ b/src/Relation/Unary/Properties.agda @@ -16,10 +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 using (yes; no) -open import Relation.Nullary.Product using (_×-dec_) -open import Relation.Nullary.Sum using (_⊎-dec_) -open import Relation.Nullary.Decidable using (¬?) +open import Relation.Nullary using (yes; no; _⊎-dec_; _×-dec_; ¬?) open import Function.Base using (id; _$_; _∘_) private diff --git a/src/Text/Regex/Properties.agda b/src/Text/Regex/Properties.agda index bc22aa5c4d..b198972e64 100644 --- a/src/Text/Regex/Properties.agda +++ b/src/Text/Regex/Properties.agda @@ -13,15 +13,14 @@ module Text.Regex.Properties {a e r} (P? : DecPoset a e r) where open import Data.List.Base using (List; []; _∷_) open import Data.List.Relation.Unary.All using (all?) open import Data.List.Relation.Unary.Any using (any?) -open import Data.Product using (_×_; _,_; uncurry) +open import Data.Product.Base using (_×_; _,_; uncurry) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Function.Base using (_$_) -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.Product using (_×-dec_) -open import Relation.Nullary.Sum using (_⊎-dec_) +open import Relation.Nullary.Decidable + using (Dec; yes; no; map′; ¬?; _×-dec_; _⊎-dec_) +open import Relation.Nullary.Negation + using (¬_; contradiction) import Relation.Unary as U open import Relation.Binary using (Decidable) From 6d8482dcb710e3faaca5bd7be889e2558e6141f8 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Tue, 25 Oct 2022 12:09:28 +0900 Subject: [PATCH 2/3] Some grepped refining of imports --- README/Axiom.agda | 2 +- README/Data/List/Relation/Binary/Pointwise.agda | 2 +- README/Text/Regex.agda | 2 +- src/Algebra/Apartness/Structures.agda | 2 +- src/Algebra/Bundles/Raw.agda | 2 +- src/Algebra/Construct/LexProduct/Base.agda | 2 +- src/Algebra/Construct/LexProduct/Inner.agda | 2 +- src/Algebra/Definitions.agda | 2 +- src/Algebra/Definitions/RawMagma.agda | 2 +- src/Algebra/Properties/CancellativeCommutativeSemiring.agda | 2 +- src/Algebra/Solver/CommutativeMonoid.agda | 2 +- src/Algebra/Solver/IdempotentCommutativeMonoid.agda | 2 +- src/Algebra/Solver/Ring.agda | 2 +- src/Data/Digit.agda | 2 +- src/Data/Fin/Base.agda | 2 +- src/Data/Fin/Induction.agda | 2 +- src/Data/Fin/Show.agda | 2 +- src/Data/Integer/Base.agda | 2 +- src/Data/Integer/Divisibility/Signed.agda | 2 +- src/Data/List/Base.agda | 2 +- src/Data/List/Membership/Setoid.agda | 2 +- src/Data/List/NonEmpty/Base.agda | 2 +- src/Data/List/Relation/Binary/Disjoint/Setoid.agda | 2 +- src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda | 2 +- src/Data/List/Relation/Binary/Lex/Core.agda | 2 +- .../List/Relation/Binary/Permutation/Setoid/Properties.agda | 2 +- src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda | 2 +- src/Data/List/Relation/Binary/Subset/Setoid.agda | 2 +- .../List/Relation/Ternary/Interleaving/Setoid/Properties.agda | 2 +- src/Data/List/Relation/Unary/AllPairs/Properties.agda | 2 +- src/Data/List/Relation/Unary/Linked/Properties.agda | 2 +- .../List/Relation/Unary/Sorted/TotalOrder/Properties.agda | 2 +- .../List/Relation/Unary/Unique/Propositional/Properties.agda | 2 +- src/Data/List/Relation/Unary/Unique/Setoid.agda | 2 +- src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda | 2 +- src/Data/List/Sort/MergeSort.agda | 4 ++-- src/Data/Maybe/Properties.agda | 2 +- src/Data/Nat/Base.agda | 2 +- src/Data/Nat/Binary/Base.agda | 2 +- src/Data/Nat/Combinatorics/Specification.agda | 2 +- src/Data/Nat/DivMod.agda | 2 +- src/Data/Nat/DivMod/Core.agda | 2 +- src/Data/Nat/Divisibility.agda | 2 +- src/Data/Nat/Divisibility/Core.agda | 2 +- src/Data/Nat/GCD.agda | 2 +- src/Data/Nat/InfinitelyOften.agda | 2 +- src/Data/Rational/Unnormalised/Base.agda | 2 +- src/Data/Sign/Base.agda | 2 +- src/Data/Sign/Properties.agda | 2 +- src/Data/String.agda | 2 +- src/Data/String/Base.agda | 2 +- src/Data/String/Properties.agda | 2 +- src/Data/Sum/Properties.agda | 2 +- src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda | 2 +- src/Data/Tree/AVL/Key.agda | 2 +- src/Data/Vec/Base.agda | 2 +- src/Data/Vec/Membership/DecSetoid.agda | 2 +- src/Data/Vec/Membership/Setoid.agda | 2 +- src/Data/Vec/Relation/Unary/Any/Properties.agda | 2 +- src/Data/Vec/Relation/Unary/Linked/Properties.agda | 2 +- .../Vec/Relation/Unary/Unique/Propositional/Properties.agda | 2 +- src/Data/Vec/Relation/Unary/Unique/Setoid.agda | 2 +- src/Data/W.agda | 2 +- src/Data/W/Sized.agda | 2 +- src/Function/Consequences.agda | 2 +- src/Function/Metric/Definitions.agda | 2 +- src/Reflection/AST/Argument/Information.agda | 2 +- src/Reflection/AST/Show.agda | 2 +- src/Relation/Binary/Bundles.agda | 2 +- src/Relation/Binary/Construct/NaturalOrder/Left.agda | 2 +- src/Relation/Binary/Construct/NaturalOrder/Right.agda | 2 +- src/Relation/Binary/Indexed/Homogeneous/Bundles.agda | 2 +- src/Relation/Binary/Morphism/RelMonomorphism.agda | 2 +- src/Relation/Binary/Properties/ApartnessRelation.agda | 2 +- src/Relation/Binary/Properties/DecTotalOrder.agda | 2 +- src/Relation/Binary/Properties/Setoid.agda | 2 +- src/Relation/Binary/Properties/TotalOrder.agda | 2 +- src/Relation/Binary/PropositionalEquality.agda | 2 +- src/Relation/Binary/Reasoning/Base/Double.agda | 2 +- src/Relation/Binary/Reasoning/Base/Partial.agda | 2 +- src/Relation/Binary/Reasoning/Base/Triple.agda | 2 +- src/Relation/Nullary/Implication.agda | 2 +- src/Relation/Nullary/Product.agda | 2 +- src/Relation/Nullary/Sum.agda | 2 +- src/Relation/Unary/Indexed.agda | 2 +- src/Relation/Unary/Polymorphic/Properties.agda | 2 +- src/Relation/Unary/Properties.agda | 2 +- src/Test/Golden.agda | 2 +- src/Text/Pretty/Core.agda | 2 +- src/Text/Regex/Base.agda | 2 +- src/Text/Regex/Derivative/Brzozowski.agda | 2 +- src/Text/Regex/SmartConstructors.agda | 2 +- tests/reflection/assumption/Main.agda | 2 +- 93 files changed, 94 insertions(+), 94 deletions(-) diff --git a/README/Axiom.agda b/README/Axiom.agda index d22dfc0ca9..43805af9c5 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 using (Dec) +open import Relation.Nullary.Decidable 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/List/Relation/Binary/Pointwise.agda b/README/Data/List/Relation/Binary/Pointwise.agda index 6b0bc17e00..4932413ad4 100644 --- a/README/Data/List/Relation/Binary/Pointwise.agda +++ b/README/Data/List/Relation/Binary/Pointwise.agda @@ -10,7 +10,7 @@ open import Data.Nat using (ℕ; _<_; s≤s; z≤n) open import Data.List using (List; []; _∷_; length) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; setoid) -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) ------------------------------------------------------------------------ -- Pointwise diff --git a/README/Text/Regex.agda b/README/Text/Regex.agda index 7a23eb9928..5b4ce805c0 100644 --- a/README/Text/Regex.agda +++ b/README/Text/Regex.agda @@ -12,7 +12,7 @@ open import Data.Bool using (true; false) open import Data.List using (_∷_; []) open import Data.String open import Function.Base using () renaming (_$′_ to _$_) -open import Relation.Nullary using (yes) +open import Relation.Nullary.Decidable using (yes) open import Relation.Nullary.Decidable using (True; False; from-yes) -- Our library available via the Text.Regex module is safe but it works on diff --git a/src/Algebra/Apartness/Structures.agda b/src/Algebra/Apartness/Structures.agda index e8a8a61b28..bf07ac14c1 100644 --- a/src/Algebra/Apartness/Structures.agda +++ b/src/Algebra/Apartness/Structures.agda @@ -22,7 +22,7 @@ open import Algebra.Definitions _≈_ using (Invertible) open import Algebra.Structures _≈_ using (IsCommutativeRing) open import Relation.Binary.Structures using (IsEquivalence; IsApartnessRelation) open import Relation.Binary.Definitions using (Tight) -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) import Relation.Binary.Properties.ApartnessRelation as AR diff --git a/src/Algebra/Bundles/Raw.agda b/src/Algebra/Bundles/Raw.agda index 2b55574f74..d793d558fe 100644 --- a/src/Algebra/Bundles/Raw.agda +++ b/src/Algebra/Bundles/Raw.agda @@ -11,7 +11,7 @@ module Algebra.Bundles.Raw where open import Algebra.Core open import Relation.Binary.Core using (Rel) open import Level using (suc; _⊔_) -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) ------------------------------------------------------------------------ -- Raw bundles with 1 binary operation diff --git a/src/Algebra/Construct/LexProduct/Base.agda b/src/Algebra/Construct/LexProduct/Base.agda index 6bc8027da8..0a0934ac9e 100644 --- a/src/Algebra/Construct/LexProduct/Base.agda +++ b/src/Algebra/Construct/LexProduct/Base.agda @@ -11,7 +11,7 @@ open import Data.Bool.Base using (true; false) open import Data.Product using (_×_; _,_) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Definitions using (Decidable) -open import Relation.Nullary using (does; yes; no) +open import Relation.Nullary.Decidable using (does; yes; no) module Algebra.Construct.LexProduct.Base {a b ℓ} {A : Set a} {B : Set b} diff --git a/src/Algebra/Construct/LexProduct/Inner.agda b/src/Algebra/Construct/LexProduct/Inner.agda index 585e868961..d2312c7985 100644 --- a/src/Algebra/Construct/LexProduct/Inner.agda +++ b/src/Algebra/Construct/LexProduct/Inner.agda @@ -12,7 +12,7 @@ open import Data.Product 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 using (does; yes; no) +open import Relation.Nullary.Decidable using (does; yes; no) open import Relation.Nullary.Negation using (contradiction; contradiction₂) import Relation.Binary.Reasoning.Setoid as SetoidReasoning diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index 9947f2f84b..e0833a78be 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -16,7 +16,7 @@ {-# OPTIONS --without-K --safe #-} open import Relation.Binary.Core -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) module Algebra.Definitions {a ℓ} {A : Set a} -- The underlying set diff --git a/src/Algebra/Definitions/RawMagma.agda b/src/Algebra/Definitions/RawMagma.agda index fd1db803b5..bf056f035b 100644 --- a/src/Algebra/Definitions/RawMagma.agda +++ b/src/Algebra/Definitions/RawMagma.agda @@ -14,7 +14,7 @@ open import Algebra.Bundles using (RawMagma) open import Data.Product using (_×_; ∃) open import Level using (_⊔_) open import Relation.Binary.Core -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) module Algebra.Definitions.RawMagma {a ℓ} (M : RawMagma a ℓ) diff --git a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda index 081050800a..84dadf83f9 100644 --- a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda +++ b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda @@ -10,7 +10,7 @@ open import Algebra using (CancellativeCommutativeSemiring) open import Algebra.Definitions using (AlmostRightCancellative) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Relation.Binary using (Decidable) -open import Relation.Nullary using (yes; no) +open import Relation.Nullary.Decidable using (yes; no) open import Relation.Nullary.Negation using (contradiction) module Algebra.Properties.CancellativeCommutativeSemiring diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda index fbf8527478..263800030d 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 as P using (_≡_; decSetoid) -open import Relation.Nullary using (Dec) +open import Relation.Nullary.Decidable using (Dec) open CommutativeMonoid M open EqReasoning setoid diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda index 2a58559d78..348d04d26b 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 using (Dec) +open import Relation.Nullary.Decidable using (Dec) module Algebra.Solver.IdempotentCommutativeMonoid {m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where diff --git a/src/Algebra/Solver/Ring.agda b/src/Algebra/Solver/Ring.agda index b379618ecd..c30e6e1c24 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 using (yes; no) +open import Relation.Nullary.Decidable using (yes; no) open import Relation.Binary.Reasoning.Setoid setoid import Relation.Binary.PropositionalEquality as PropEq import Relation.Binary.Reflection as Reflection diff --git a/src/Data/Digit.agda b/src/Data/Digit.agda index d8c67ca730..a520b9f08d 100644 --- a/src/Data/Digit.agda +++ b/src/Data/Digit.agda @@ -19,7 +19,7 @@ open import Data.Product open import Data.Vec.Base as Vec using (Vec; _∷_; []) open import Data.Nat.DivMod open import Data.Nat.Induction -open import Relation.Nullary using (does) +open import Relation.Nullary.Decidable using (does) open import Relation.Nullary.Decidable open import Relation.Binary using (Decidable) open import Relation.Binary.PropositionalEquality as P using (_≡_; refl) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index 06c4581337..09e204d365 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -18,7 +18,7 @@ open import Data.Product 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 using (yes; no) +open import Relation.Nullary.Decidable using (yes; no) open import Relation.Nullary.Negation using (contradiction) open import Relation.Nullary.Decidable.Core using (True; toWitness) open import Relation.Binary.Core diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda index 401c95b38a..76bbde2de1 100644 --- a/src/Data/Fin/Induction.agda +++ b/src/Data/Fin/Induction.agda @@ -27,7 +27,7 @@ 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 using (yes; no) +open import Relation.Nullary.Decidable using (yes; no) open import Relation.Nullary.Negation using (contradiction) open import Relation.Unary using (Pred) diff --git a/src/Data/Fin/Show.agda b/src/Data/Fin/Show.agda index f9816e4900..bf101ee99c 100644 --- a/src/Data/Fin/Show.agda +++ b/src/Data/Fin/Show.agda @@ -14,7 +14,7 @@ open import Data.Nat as ℕ using (ℕ; _≤?_; __; z) open import Relation.Unary using (Pred) -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) open import Relation.Nullary.Negation using (contradiction) open import Data.Tree.AVL.Indexed sto as AVL diff --git a/src/Data/Tree/AVL/Key.agda b/src/Data/Tree/AVL/Key.agda index 77063c49d6..7a3ee66050 100644 --- a/src/Data/Tree/AVL/Key.agda +++ b/src/Data/Tree/AVL/Key.agda @@ -18,7 +18,7 @@ open import Data.Empty open import Data.Unit open import Data.Product open import Relation.Binary.PropositionalEquality using (_≡_ ; refl) -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) open import Relation.Nullary.Construct.Add.Extrema as AddExtremaToSet using (_±) import Relation.Binary.Construct.Add.Extrema.Equality diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index d25c2384c8..c7ea56174a 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -17,7 +17,7 @@ open import Data.These.Base as These using (These; this; that; these) open import Function.Base using (const; _∘′_; id; _∘_) open import Level using (Level) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong) -open import Relation.Nullary using (does) +open import Relation.Nullary.Decidable using (does) open import Relation.Unary using (Pred; Decidable) private diff --git a/src/Data/Vec/Membership/DecSetoid.agda b/src/Data/Vec/Membership/DecSetoid.agda index c1b4e1e916..a9ff2d58ea 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 using (Dec) +open import Relation.Nullary.Decidable using (Dec) open DecSetoid DS renaming (Carrier to A) ------------------------------------------------------------------------ diff --git a/src/Data/Vec/Membership/Setoid.agda b/src/Data/Vec/Membership/Setoid.agda index a03befdb39..68be682e7d 100644 --- a/src/Data/Vec/Membership/Setoid.agda +++ b/src/Data/Vec/Membership/Setoid.agda @@ -15,7 +15,7 @@ open import Data.Vec.Base as Vec using (Vec; []; _∷_) open import Data.Vec.Relation.Unary.Any as Any using (Any; here; there; index) open import Data.Product using (∃; _×_; _,_) -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) open import Relation.Unary using (Pred) open Setoid S renaming (Carrier to A) diff --git a/src/Data/Vec/Relation/Unary/Any/Properties.agda b/src/Data/Vec/Relation/Unary/Any/Properties.agda index 9faa49d464..17040a4862 100644 --- a/src/Data/Vec/Relation/Unary/Any/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Any/Properties.agda @@ -26,7 +26,7 @@ open import Function.Base open import Function.Inverse using (_↔_; inverse) renaming (_∘_ to _∘↔_; id to id↔) open import Level using (Level) -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) open import Relation.Unary hiding (_∈_) open import Relation.Binary open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_; refl) diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda index 3935a263c4..8fa3157bde 100644 --- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda @@ -22,7 +22,7 @@ open import Function.Base using (_∘_; flip; _on_) open import Relation.Binary using (Rel; Transitive; DecSetoid) open import Relation.Binary.PropositionalEquality using (_≢_) open import Relation.Unary using (Pred; Decidable) -open import Relation.Nullary using (yes; no; does) +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 acd1b916c8..e740fd8ad2 100644 --- a/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda @@ -24,7 +24,7 @@ open import Relation.Binary using (Rel; Setoid) open import Relation.Binary.PropositionalEquality using (refl; _≡_; _≢_; sym; setoid) open import Relation.Unary using (Pred; Decidable) -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) private variable diff --git a/src/Data/Vec/Relation/Unary/Unique/Setoid.agda b/src/Data/Vec/Relation/Unary/Unique/Setoid.agda index fae3073b9e..dd5cbb0c37 100644 --- a/src/Data/Vec/Relation/Unary/Unique/Setoid.agda +++ b/src/Data/Vec/Relation/Unary/Unique/Setoid.agda @@ -16,7 +16,7 @@ open import Data.Vec.Base import Data.Vec.Relation.Unary.AllPairs as AllPairsM open import Level using (_⊔_) open import Relation.Unary using (Pred) -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) ------------------------------------------------------------------------ diff --git a/src/Data/W.agda b/src/Data/W.agda index fc9464e8c9..81902e5a63 100644 --- a/src/Data/W.agda +++ b/src/Data/W.agda @@ -13,7 +13,7 @@ open import Function.Base using (_$_; _∘_; const) open import Data.Product using (_,_; -,_; proj₂) open import Data.Container.Core using (Container; ⟦_⟧; Shape; Position; _⇒_; ⟪_⟫) open import Data.Container.Relation.Unary.All using (□; all) -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) open import Agda.Builtin.Equality using (_≡_; refl) private diff --git a/src/Data/W/Sized.agda b/src/Data/W/Sized.agda index 655ab2911d..d977128900 100644 --- a/src/Data/W/Sized.agda +++ b/src/Data/W/Sized.agda @@ -14,7 +14,7 @@ open import Function.Base using (_$_; _∘_; const) open import Data.Product using (_,_; -,_; proj₂) open import Data.Container.Core as Container using (Container; ⟦_⟧; Shape; Position; _⇒_; ⟪_⟫) open import Data.Container.Relation.Unary.All using (□; all) -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) open import Relation.Binary.PropositionalEquality using (_≡_; refl) private diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda index 0c98c0c2a1..e2c51e90d6 100644 --- a/src/Function/Consequences.agda +++ b/src/Function/Consequences.agda @@ -13,7 +13,7 @@ open import Function.Definitions open import Level open import Relation.Binary import Relation.Binary.Reasoning.Setoid as SetoidReasoning -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) open import Relation.Nullary.Negation.Core using (contraposition) private diff --git a/src/Function/Metric/Definitions.agda b/src/Function/Metric/Definitions.agda index e95e7b26a0..adf343aebb 100644 --- a/src/Function/Metric/Definitions.agda +++ b/src/Function/Metric/Definitions.agda @@ -15,7 +15,7 @@ open import Data.Product using (∃) open import Function.Metric.Core using (DistanceFunction) open import Level using (Level) open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_) -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) private variable diff --git a/src/Reflection/AST/Argument/Information.agda b/src/Reflection/AST/Argument/Information.agda index 7838f016bc..084ea24ea9 100644 --- a/src/Reflection/AST/Argument/Information.agda +++ b/src/Reflection/AST/Argument/Information.agda @@ -10,7 +10,7 @@ module Reflection.AST.Argument.Information where open import Data.Product.Base import Relation.Nullary.Decidable as Dec -open import Relation.Nullary using (_×-dec_) +open import Relation.Nullary.Decidable using (_×-dec_) open import Relation.Binary open import Relation.Binary.PropositionalEquality diff --git a/src/Reflection/AST/Show.agda b/src/Reflection/AST/Show.agda index 8c14238669..66341ae7ed 100644 --- a/src/Reflection/AST/Show.agda +++ b/src/Reflection/AST/Show.agda @@ -19,7 +19,7 @@ import Data.Nat.Show as ℕ open import Data.Product using (_×_; _,_) open import Data.String as String import Data.Word as Word -open import Relation.Nullary using (yes; no) +open import Relation.Nullary.Decidable using (yes; no) open import Function.Base using (id; _∘′_; case_of_) open import Reflection.AST.Abstraction hiding (map) diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda index 4c4cd9b8e3..2c8b94082c 100644 --- a/src/Relation/Binary/Bundles.agda +++ b/src/Relation/Binary/Bundles.agda @@ -11,7 +11,7 @@ module Relation.Binary.Bundles where open import Level -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) open import Relation.Binary.Core open import Relation.Binary.Definitions open import Relation.Binary.Structures diff --git a/src/Relation/Binary/Construct/NaturalOrder/Left.agda b/src/Relation/Binary/Construct/NaturalOrder/Left.agda index c36a314d99..aa51ef60b9 100644 --- a/src/Relation/Binary/Construct/NaturalOrder/Left.agda +++ b/src/Relation/Binary/Construct/NaturalOrder/Left.agda @@ -11,7 +11,7 @@ open import Algebra.Core open import Data.Product using (_,_; _×_) open import Data.Sum.Base using (inj₁; inj₂) open import Relation.Binary -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) import Relation.Binary.Reasoning.Setoid as EqReasoning open import Relation.Binary.Lattice using (Infimum) diff --git a/src/Relation/Binary/Construct/NaturalOrder/Right.agda b/src/Relation/Binary/Construct/NaturalOrder/Right.agda index b3ee31e03f..ad4c78f9ea 100644 --- a/src/Relation/Binary/Construct/NaturalOrder/Right.agda +++ b/src/Relation/Binary/Construct/NaturalOrder/Right.agda @@ -11,7 +11,7 @@ open import Algebra.Core using (Op₂) open import Data.Product using (_,_; _×_) open import Data.Sum.Base using (inj₁; inj₂) open import Relation.Binary -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) import Relation.Binary.Reasoning.Setoid as EqReasoning module Relation.Binary.Construct.NaturalOrder.Right diff --git a/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda b/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda index 80f4d74bb6..3618d3dea3 100644 --- a/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda +++ b/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda @@ -16,7 +16,7 @@ open import Function.Base using (_⟨_⟩_) open import Level using (Level; _⊔_; suc) open import Relation.Binary as B using (_⇒_) open import Relation.Binary.PropositionalEquality as P using (_≡_) -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) open import Relation.Binary.Indexed.Homogeneous.Core open import Relation.Binary.Indexed.Homogeneous.Structures diff --git a/src/Relation/Binary/Morphism/RelMonomorphism.agda b/src/Relation/Binary/Morphism/RelMonomorphism.agda index 1b27014052..5da0d18524 100644 --- a/src/Relation/Binary/Morphism/RelMonomorphism.agda +++ b/src/Relation/Binary/Morphism/RelMonomorphism.agda @@ -20,7 +20,7 @@ module Relation.Binary.Morphism.RelMonomorphism where open import Data.Sum.Base as Sum -open import Relation.Nullary using (yes; no) +open import Relation.Nullary.Decidable using (yes; no) open import Relation.Nullary.Decidable open IsRelMonomorphism isMonomorphism diff --git a/src/Relation/Binary/Properties/ApartnessRelation.agda b/src/Relation/Binary/Properties/ApartnessRelation.agda index 1a7f392d36..c043135852 100644 --- a/src/Relation/Binary/Properties/ApartnessRelation.agda +++ b/src/Relation/Binary/Properties/ApartnessRelation.agda @@ -18,7 +18,7 @@ open import Function.Base using (_∘₂_) open import Relation.Binary.Definitions using (Reflexive) open import Relation.Binary.Consequences using (sym⇒¬-sym; cotrans⇒¬-trans) open import Relation.Binary.Structures using (IsEquivalence; IsApartnessRelation) -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) ¬#-isEquivalence : Reflexive _≈_ → IsApartnessRelation _≈_ _#_ → IsEquivalence (¬_ ∘₂ _#_) diff --git a/src/Relation/Binary/Properties/DecTotalOrder.agda b/src/Relation/Binary/Properties/DecTotalOrder.agda index 289aae812e..c3589b01ad 100644 --- a/src/Relation/Binary/Properties/DecTotalOrder.agda +++ b/src/Relation/Binary/Properties/DecTotalOrder.agda @@ -16,7 +16,7 @@ open DecTotalOrder DT hiding (trans) import Relation.Binary.Construct.Converse as Converse import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict import Relation.Binary.Properties.TotalOrder totalOrder as TotalOrderProperties -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) ------------------------------------------------------------------------ -- _≥_ - the flipped relation is also a total order diff --git a/src/Relation/Binary/Properties/Setoid.agda b/src/Relation/Binary/Properties/Setoid.agda index 66aa8694cd..74174d6de1 100644 --- a/src/Relation/Binary/Properties/Setoid.agda +++ b/src/Relation/Binary/Properties/Setoid.agda @@ -8,7 +8,7 @@ open import Data.Product using (_,_) open import Function.Base using (_∘_; id; _$_; flip) -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) open import Relation.Binary diff --git a/src/Relation/Binary/Properties/TotalOrder.agda b/src/Relation/Binary/Properties/TotalOrder.agda index b2bdb66e31..dc18df5dd1 100644 --- a/src/Relation/Binary/Properties/TotalOrder.agda +++ b/src/Relation/Binary/Properties/TotalOrder.agda @@ -19,7 +19,7 @@ import Relation.Binary.Construct.Converse as Converse import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict import Relation.Binary.Properties.Poset poset as PosetProperties open import Relation.Binary.Consequences -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) open import Relation.Nullary.Negation using (contradiction) ------------------------------------------------------------------------ diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda index 12a79f13ed..4c7e71b2cd 100644 --- a/src/Relation/Binary/PropositionalEquality.agda +++ b/src/Relation/Binary/PropositionalEquality.agda @@ -15,7 +15,7 @@ open import Function.Equality using (Π; _⟶_; ≡-setoid) open import Level using (Level; _⊔_) open import Data.Product using (∃) -open import Relation.Nullary using (yes ; no) +open import Relation.Nullary.Decidable using (yes; no) open import Relation.Nullary.Decidable open import Relation.Binary open import Relation.Binary.Indexed.Heterogeneous diff --git a/src/Relation/Binary/Reasoning/Base/Double.agda b/src/Relation/Binary/Reasoning/Base/Double.agda index f30636ba64..1b092c2c5f 100644 --- a/src/Relation/Binary/Reasoning/Base/Double.agda +++ b/src/Relation/Binary/Reasoning/Base/Double.agda @@ -21,7 +21,7 @@ open import Level using (Level; _⊔_; Lift; lift) open import Function.Base using (case_of_; id) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym) -open import Relation.Nullary using (Dec; yes; no) +open import Relation.Nullary.Decidable using (Dec; yes; no) open import Relation.Nullary.Decidable using (True; toWitness) open IsPreorder isPreorder diff --git a/src/Relation/Binary/Reasoning/Base/Partial.agda b/src/Relation/Binary/Reasoning/Base/Partial.agda index dd60628c4c..46d5a27ba0 100644 --- a/src/Relation/Binary/Reasoning/Base/Partial.agda +++ b/src/Relation/Binary/Reasoning/Base/Partial.agda @@ -11,7 +11,7 @@ open import Relation.Binary.Definitions open import Level using (_⊔_) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) -open import Relation.Nullary using (Dec; yes; no) +open import Relation.Nullary.Decidable using (Dec; yes; no) open import Relation.Nullary.Decidable using (True) module Relation.Binary.Reasoning.Base.Partial diff --git a/src/Relation/Binary/Reasoning/Base/Triple.agda b/src/Relation/Binary/Reasoning/Base/Triple.agda index 32c384d24c..b44f61226e 100644 --- a/src/Relation/Binary/Reasoning/Base/Triple.agda +++ b/src/Relation/Binary/Reasoning/Base/Triple.agda @@ -24,7 +24,7 @@ open import Function.Base using (case_of_; id) open import Level using (Level; _⊔_; Lift; lift) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym) -open import Relation.Nullary using (Dec; yes; no) +open import Relation.Nullary.Decidable using (Dec; yes; no) open import Relation.Nullary.Decidable using (True; toWitness) open IsPreorder isPreorder diff --git a/src/Relation/Nullary/Implication.agda b/src/Relation/Nullary/Implication.agda index 65ab98fe1d..ff5674f5df 100644 --- a/src/Relation/Nullary/Implication.agda +++ b/src/Relation/Nullary/Implication.agda @@ -10,7 +10,7 @@ module Relation.Nullary.Implication where {-# WARNING_ON_IMPORT "Relation.Nullary.Implication was deprecated in v2.0. -Use `Relation.Nullary` instead." +Use `Relation.Nullary.Decidable` or `Relation.Nullary` instead." #-} open import Relation.Nullary.Decidable.Core public using (_→-dec_) diff --git a/src/Relation/Nullary/Product.agda b/src/Relation/Nullary/Product.agda index ca2a52bdb6..0998a7aec0 100644 --- a/src/Relation/Nullary/Product.agda +++ b/src/Relation/Nullary/Product.agda @@ -10,7 +10,7 @@ module Relation.Nullary.Product where {-# WARNING_ON_IMPORT "Relation.Nullary.Product was deprecated in v2.0. -Use `Relation.Nullary` instead." +Use `Relation.Nullary.Decidable` or `Relation.Nullary` instead." #-} open import Relation.Nullary.Decidable.Core public using (_×-dec_) diff --git a/src/Relation/Nullary/Sum.agda b/src/Relation/Nullary/Sum.agda index 6860b9a643..4d66cb0ad2 100644 --- a/src/Relation/Nullary/Sum.agda +++ b/src/Relation/Nullary/Sum.agda @@ -10,7 +10,7 @@ module Relation.Nullary.Sum where {-# WARNING_ON_IMPORT "Relation.Nullary.Sum was deprecated in v2.0. -Use `Relation.Nullary` instead." +Use `Relation.Nullary.Decidable` or `Relation.Nullary` instead." #-} open import Relation.Nullary.Negation.Core public using (_¬-⊎_) diff --git a/src/Relation/Unary/Indexed.agda b/src/Relation/Unary/Indexed.agda index 8ce3622ce3..49e36d3679 100644 --- a/src/Relation/Unary/Indexed.agda +++ b/src/Relation/Unary/Indexed.agda @@ -10,7 +10,7 @@ module Relation.Unary.Indexed where open import Data.Product using (∃; _×_) open import Level -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) IPred : ∀ {i a} {I : Set i} → (I → Set a) → (ℓ : Level) → Set _ IPred A ℓ = ∀ {i} → A i → Set ℓ diff --git a/src/Relation/Unary/Polymorphic/Properties.agda b/src/Relation/Unary/Polymorphic/Properties.agda index e40a29c361..61b25678b9 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 using (yes; no) +open import Relation.Nullary.Decidable 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 5cdbcb6015..0dc39837b3 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 using (yes; no; _⊎-dec_; _×-dec_; ¬?) +open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_; ¬?) open import Function.Base using (id; _$_; _∘_) private diff --git a/src/Test/Golden.agda b/src/Test/Golden.agda index ffa98b22d6..16e03a95df 100644 --- a/src/Test/Golden.agda +++ b/src/Test/Golden.agda @@ -96,7 +96,7 @@ open import Data.Unit.Base using (⊤) open import Function.Base using (id; _$_; case_of_) -open import Relation.Nullary using (does) +open import Relation.Nullary.Decidable using (does) open import Codata.Musical.Notation using (♯_) open import IO diff --git a/src/Text/Pretty/Core.agda b/src/Text/Pretty/Core.agda index e09d9e66b5..f546bc5962 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 using (Dec) +open import Relation.Nullary.Decidable using (Dec) open import Relation.Unary using (IUniversal; _⇒_; U) open import Relation.Binary.PropositionalEquality diff --git a/src/Text/Regex/Base.agda b/src/Text/Regex/Base.agda index d2d1003318..adfde3e03d 100644 --- a/src/Text/Regex/Base.agda +++ b/src/Text/Regex/Base.agda @@ -18,7 +18,7 @@ open import Data.List.Relation.Unary.Any using (Any) open import Data.List.Relation.Unary.All using (All) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) -open import Relation.Nullary using (¬_) +open import Relation.Nullary.Negation using (¬_) open import Relation.Nullary.Negation using (contradiction) open import Relation.Unary using (Pred) open import Relation.Binary.PropositionalEquality diff --git a/src/Text/Regex/Derivative/Brzozowski.agda b/src/Text/Regex/Derivative/Brzozowski.agda index e1aa7bdcc0..57dd1f165d 100644 --- a/src/Text/Regex/Derivative/Brzozowski.agda +++ b/src/Text/Regex/Derivative/Brzozowski.agda @@ -15,7 +15,7 @@ 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 using (Dec; yes; no) +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.Binary using (Decidable) diff --git a/src/Text/Regex/SmartConstructors.agda b/src/Text/Regex/SmartConstructors.agda index a9f2fb2a14..e27ae2a1d3 100644 --- a/src/Text/Regex/SmartConstructors.agda +++ b/src/Text/Regex/SmartConstructors.agda @@ -17,7 +17,7 @@ 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 using (yes; no) +open import Relation.Nullary.Decidable using (yes; no) open import Relation.Nullary.Negation using (contradiction) open import Relation.Binary.PropositionalEquality using (refl) diff --git a/tests/reflection/assumption/Main.agda b/tests/reflection/assumption/Main.agda index 5146743bde..d7f30d3118 100644 --- a/tests/reflection/assumption/Main.agda +++ b/tests/reflection/assumption/Main.agda @@ -16,7 +16,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 using (does) +open import Relation.Nullary.Decidable using (does) open import Effect.Monad open RawMonad {{...}} From 5ca5874bbc04a5d539b4b5c788c9382b6044eb68 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Sun, 30 Oct 2022 11:08:32 +0900 Subject: [PATCH 3/3] Added missing deprecation warnings --- src/Relation/Nullary/Implication.agda | 2 +- src/Relation/Nullary/Product.agda | 2 +- src/Relation/Nullary/Sum.agda | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Relation/Nullary/Implication.agda b/src/Relation/Nullary/Implication.agda index ff5674f5df..90ff3514e1 100644 --- a/src/Relation/Nullary/Implication.agda +++ b/src/Relation/Nullary/Implication.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Implications of nullary relations +-- This module is DEPRECATED. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} diff --git a/src/Relation/Nullary/Product.agda b/src/Relation/Nullary/Product.agda index 0998a7aec0..0d87c30fcc 100644 --- a/src/Relation/Nullary/Product.agda +++ b/src/Relation/Nullary/Product.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Products of nullary relations +-- This module is DEPRECATED. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} diff --git a/src/Relation/Nullary/Sum.agda b/src/Relation/Nullary/Sum.agda index 4d66cb0ad2..b46fbf9545 100644 --- a/src/Relation/Nullary/Sum.agda +++ b/src/Relation/Nullary/Sum.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Sums of nullary relations +-- This module is DEPRECATED. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-}