Skip to content

Stage 2 of refactoring of Relation.Nullary #1869

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Oct 30, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 10 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
Expand Down
2 changes: 1 addition & 1 deletion README/Axiom.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
2 changes: 1 addition & 1 deletion README/Data/List/Relation/Binary/Pointwise.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
18 changes: 10 additions & 8 deletions README/Design/Decidability.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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 _≟₀_ _≟₁_ _≟₂_

Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion README/Text/Regex.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Algebra/Apartness/Structures.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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


Expand Down
2 changes: 1 addition & 1 deletion src/Algebra/Bundles/Raw.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Algebra/Construct/LexProduct/Base.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down
2 changes: 1 addition & 1 deletion src/Algebra/Construct/LexProduct/Inner.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Algebra/Definitions.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Algebra/Definitions/RawMagma.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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 ℓ)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Algebra/Solver/CommutativeMonoid.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Algebra/Solver/IdempotentCommutativeMonoid.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Algebra/Solver/Ring.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Digit.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Fin/Base.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Fin/Induction.agda
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,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)

Expand Down
9 changes: 3 additions & 6 deletions src/Data/Fin/Properties.agda
Original file line number Diff line number Diff line change
Expand Up @@ -37,13 +37,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?)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Fin/Show.agda
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ open import Data.Nat as ℕ using (ℕ; _≤?_; _<?_)
import Data.Nat.Show as ℕ
open import Data.String.Base using (String)
open import Function.Base
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (yes; no)
open import Relation.Nullary.Decidable using (True)

show : ∀ {n} → Fin n → String
Expand Down
4 changes: 1 addition & 3 deletions src/Data/Fin/Subset/Properties.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Integer/Base.agda
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ open import Level using (0ℓ)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; _≢_; refl)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (¬_)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Unary using (Pred)

Expand Down
2 changes: 1 addition & 1 deletion src/Data/Integer/Divisibility/Signed.agda
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
import Relation.Binary.Reasoning.Preorder as PreorderReasoning
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (yes; no)
import Relation.Nullary.Decidable as DEC

------------------------------------------------------------------------
Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Base.agda
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
open import Data.These.Base as These using (These; this; that; these)
open import Function.Base using (id; _∘_ ; _∘′_; _∘₂_; const; flip)
open import Level using (Level)
open import Relation.Nullary using (does)
open import Relation.Nullary.Decidable using (does)
open import Relation.Nullary.Decidable using (¬?)
open import Relation.Unary using (Pred; Decidable)
open import Relation.Unary.Properties using (∁?)
Expand Down
4 changes: 1 addition & 3 deletions src/Data/List/Fresh/Relation/Unary/All.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
5 changes: 2 additions & 3 deletions src/Data/List/Fresh/Relation/Unary/Any.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Membership/Setoid.agda
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ open import Data.List.Relation.Unary.Any
using (Any; index; map; here; there)
open import Data.Product as Prod using (∃; _×_; _,_)
open import Relation.Unary using (Pred)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (¬_)

open Setoid S renaming (Carrier to A)

Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/NonEmpty/Base.agda
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ open import Relation.Binary.PropositionalEquality.Core
using (_≡_; _≢_; refl)
open import Relation.Unary using (Pred; Decidable; U; ∅)
open import Relation.Unary.Properties using (U?; ∅?)
open import Relation.Nullary using (does)
open import Relation.Nullary.Decidable using (does)

private
variable
Expand Down
6 changes: 2 additions & 4 deletions src/Data/List/Properties.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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 (∁?)

Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Relation/Binary/Disjoint/Setoid.agda
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ open import Relation.Binary
module Data.List.Relation.Binary.Disjoint.Setoid {c ℓ} (S : Setoid c ℓ) where

open import Level using (_⊔_)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (¬_)
open import Function.Base using (_∘_)
open import Data.List.Base using (List; []; [_]; _∷_)
open import Data.List.Relation.Unary.Any using (here; there)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ open import Data.List.Relation.Unary.Any.Properties using (++⁻)
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 (¬_)

------------------------------------------------------------------------
-- Relational properties
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
7 changes: 3 additions & 4 deletions src/Data/List/Relation/Binary/Lex.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Relation/Binary/Lex/Core.agda
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ open import Data.Product using (_×_; _,_; proj₁; proj₂; uncurry)
open import Data.List.Base using (List; []; _∷_)
open import Function.Base using (_∘_; flip; id)
open import Level using (Level; _⊔_)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (¬_)
open import Relation.Binary.Core using (Rel)
open import Data.List.Relation.Binary.Pointwise.Base
using (Pointwise; []; _∷_; head; tail)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ open import Relation.Unary using (Pred; Decidable)
open import Relation.Binary.Properties.Setoid S using (≉-resp₂)
open import Relation.Binary.PropositionalEquality as ≡
using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_; inspect)
open import Relation.Nullary using (yes; no; does)
open import Relation.Nullary.Decidable using (yes; no; does)
open import Relation.Nullary.Negation using (contradiction)

private
Expand Down
2 changes: 0 additions & 2 deletions src/Data/List/Relation/Binary/Pointwise.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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 (_≡_)
Expand Down
Loading