Skip to content
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.

Sign up for GitHub

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

Simplify more Relation.Binary imports #2034

Merged
merged 4 commits into from
Jul 29, 2023
Merged

Simplify more Relation.Binary imports #2034

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
7697758
Simplify more `Relation.Binary` imports
Saransh-cpp Jun 25, 2023
0dfd39a
Better naming scheme
Saransh-cpp Jun 28, 2023
69f765e
Resolve conflicts
Saransh-cpp Jul 28, 2023
4460f0c
Merge branch 'master' of https://github.com/agda/agda-stdlib into Rel…
Saransh-cpp Jul 28, 2023
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
2 changes: 1 addition & 1 deletion src/Algebra/Properties/Monoid/Sum.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ open import Data.Vec.Functional as Vector
open import Data.Fin.Base using (zero; suc)
open import Data.Unit using (tt)
open import Function.Base using (_∘_)
open import Relation.Binary as B using (_Preserves_⟶_)
open import Relation.Binary.Core using (_Preserves_⟶_)
open import Relation.Binary.PropositionalEquality as P using (_≗_; _≡_)

module Algebra.Properties.Monoid.Sum {a ℓ} (M : Monoid a ℓ) where
Expand Down
2 changes: 1 addition & 1 deletion src/Data/AVL/Map.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary using (StrictTotalOrder)
open import Relation.Binary.Bundles using (StrictTotalOrder)

module Data.AVL.Map
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/AVL/NonEmpty.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary using (StrictTotalOrder)
open import Relation.Binary.Bundles using (StrictTotalOrder)

module Data.AVL.NonEmpty
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) where
Expand Down
2 changes: 1 addition & 1 deletion src/Data/AVL/Sets.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary using (StrictTotalOrder)
open import Relation.Binary.Bundles using (StrictTotalOrder)

module Data.AVL.Sets
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/AVL/Value.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary using (Setoid)
open import Relation.Binary.Bundles using (Setoid)

module Data.AVL.Value {a ℓ} (S : Setoid a ℓ) where

Expand Down
2 changes: 1 addition & 1 deletion src/Data/Container/Morphism/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ module Data.Container.Morphism.Properties where
open import Level using (_⊔_; suc)
open import Function.Base as F using (_$_)
open import Data.Product using (∃; proj₁; proj₂; _,_)
open import Relation.Binary using (Setoid)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)

open import Data.Container.Core
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Container/Relation/Binary/Equality/Setoid.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary using (Setoid)
open import Relation.Binary.Bundles using (Setoid)

module Data.Container.Relation.Binary.Equality.Setoid {c e} (S : Setoid c e) where

Expand Down
2 changes: 1 addition & 1 deletion src/Data/Container/Relation/Binary/Pointwise.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ module Data.Container.Relation.Binary.Pointwise where
open import Data.Product using (_,_; Σ-syntax; -,_; proj₁; proj₂)
open import Function
open import Level using (_⊔_)
open import Relation.Binary using (REL; _⇒_)
open import Relation.Binary.Core using (REL; _⇒_)
open import Relation.Binary.PropositionalEquality.Core as P
using (_≡_; subst; cong)

Expand Down
2 changes: 1 addition & 1 deletion src/Data/Container/Relation/Unary/Any/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ open import Function.Inverse as Inv using (_↔_; inverse; module Inverse)
open import Function.Related as Related using (Related; SK-sym)
open import Function.Related.TypeIsomorphisms
open import Relation.Unary using (Pred ; _∪_ ; _∩_)
open import Relation.Binary using (REL)
open import Relation.Binary.Core using (REL)
open import Relation.Binary.PropositionalEquality as P
using (_≡_; _≗_; refl)

Expand Down
2 changes: 1 addition & 1 deletion src/Data/Fin/Permutation.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ open import Function.Equality using (_⟨$⟩_)
open import Function.Properties.Inverse using (↔⇒↣)
open import Function.Base using (_∘_)
open import Level using (0ℓ)
open import Relation.Binary using (Rel)
open import Relation.Binary.Core using (Rel)
open import Relation.Nullary using (does; ¬_; yes; no)
open import Relation.Nullary.Decidable using (dec-yes; dec-no)
open import Relation.Nullary.Negation using (contradiction)
Expand Down
3 changes: 2 additions & 1 deletion src/Data/Integer/Coprimality.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,8 @@ import Data.Nat.Coprimality as ℕ
import Data.Nat.Divisibility as ℕ
open import Function.Base using (_on_)
open import Level using (0ℓ)
open import Relation.Binary using (Rel; Decidable; Symmetric)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions using (Decidable; Symmetric)
open import Relation.Binary.PropositionalEquality.Core using (subst)

------------------------------------------------------------------------
Expand Down
3 changes: 2 additions & 1 deletion src/Data/List/Extrema/Core.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,8 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary using (Trans; TotalOrder; Setoid)
open import Relation.Binary.Definitions using (Trans)
open import Relation.Binary.Bundles using (TotalOrder; Setoid)

module Data.List.Extrema.Core
{b ℓ₁ ℓ₂} (totalOrder : TotalOrder b ℓ₁ ℓ₂) where
Expand Down
3 changes: 2 additions & 1 deletion src/Data/List/Fresh/Membership/Setoid/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,8 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary using (Rel; Setoid)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)

module Data.List.Fresh.Membership.Setoid.Properties {c ℓ} (S : Setoid c ℓ) where

Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Fresh/Relation/Unary/All.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ open import Data.Product using (_×_; _,_; proj₁; uncurry)
open import Data.Sum.Base as Sum using (inj₁; inj₂)
open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_)
open import Relation.Unary as U
open import Relation.Binary as B using (Rel)
open import Relation.Binary.Core using (Rel)

open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
open import Data.List.Fresh.Relation.Unary.Any as Any using (Any; here; there)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Fresh/Relation/Unary/All/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ open import Data.Product using (_,_)
open import Function.Base using (_∘′_)
open import Relation.Nullary
open import Relation.Unary as U
open import Relation.Binary as B using (Rel)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)

open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Fresh/Relation/Unary/Any.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ open import Function.Bundles using (_⇔_; mk⇔)
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)
open import Relation.Binary.Core using (Rel)

open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)

Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Fresh/Relation/Unary/Any/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ open import Function.Base using (_∘′_)
open import Relation.Nullary.Reflects using (invert)
open import Relation.Nullary
open import Relation.Unary as U using (Pred)
open import Relation.Binary as B using (Rel)
open import Relation.Binary.Core using (Rel)
open import Relation.Nary
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)

Expand Down
3 changes: 2 additions & 1 deletion src/Data/List/Membership/Propositional/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,8 @@ open import Function.Inverse as Inv using (_↔_; module Inverse)
import Function.Related as Related
open import Function.Related.TypeIsomorphisms
open import Level using (Level)
open import Relation.Binary as B hiding (Decidable)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions as B hiding (Decidable)
open import Relation.Binary.PropositionalEquality as P
using (_≡_; _≢_; refl; sym; trans; cong; subst; →-to-⟶; _≗_)
import Relation.Binary.Properties.DecTotalOrder as DTOProperties
Expand Down
5 changes: 4 additions & 1 deletion src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,10 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary as B hiding (Decidable)
open import Relation.Binary.Core
using (Rel; _⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Definitions as B hiding (Decidable)

module Data.List.Relation.Binary.Permutation.Setoid.Properties
{a ℓ} (S : Setoid a ℓ)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.Relation.Binary.Pointwise
using (Pointwise; []; _∷_)
open import Data.Product using (∃; _×_; _,_; uncurry)
open import Relation.Binary using (REL; _⇒_)
open import Relation.Binary.Core using (REL; _⇒_)

module _ {a b r} {A : Set a} {B : Set b} (R : REL A B r) where

Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Relation/Binary/Sublist/DecPropositional/Solver.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary using (Decidable)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)

module Data.List.Relation.Binary.Sublist.DecPropositional.Solver
Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Relation/Binary/Sublist/DecSetoid/Solver.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary using (DecSetoid)
open import Relation.Binary.Bundles using (DecSetoid)

module Data.List.Relation.Binary.Sublist.DecSetoid.Solver {c ℓ} (S : DecSetoid c ℓ) where

Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Relation/Binary/Sublist/Heterogeneous/Core.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary using (REL)
open import Relation.Binary.Core using (REL)

module Data.List.Relation.Binary.Sublist.Heterogeneous.Core
{a b r} {A : Set a} {B : Set b} (R : REL A B r)
Expand Down
3 changes: 2 additions & 1 deletion src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,8 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary using (Rel; Reflexive; Decidable)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions using (Reflexive; Decidable)

module Data.List.Relation.Binary.Sublist.Heterogeneous.Solver
{a r} {A : Set a} (R : Rel A r)
Expand Down
3 changes: 2 additions & 1 deletion src/Data/List/Relation/Binary/Sublist/Setoid.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,8 @@
{-# OPTIONS --cubical-compatible --safe #-}
{-# OPTIONS --postfix-projections #-}

open import Relation.Binary using (Setoid; Rel)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)

module Data.List.Relation.Binary.Sublist.Setoid
{c ℓ} (S : Setoid c ℓ) where
Expand Down
6 changes: 4 additions & 2 deletions src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,8 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary hiding (Decidable)
open import Relation.Binary.Definitions hiding (Decidable)
open import Relation.Binary.Structures using (IsPreorder)

module Data.List.Relation.Binary.Subset.Propositional.Properties
where
Expand Down Expand Up @@ -35,7 +36,8 @@ open import Function.Equivalence using (module Equivalence)
open import Level using (Level)
open import Relation.Nullary using (¬_; yes; no)
open import Relation.Unary using (Decidable; Pred) renaming (_⊆_ to _⋐_)
open import Relation.Binary using (_⇒_; _Respects_)
open import Relation.Binary.Core using (_⇒_)
open import Relation.Binary.Bundles using (Preorder)
open import Relation.Binary.PropositionalEquality
using (_≡_; _≗_; isEquivalence; subst; resp; refl; setoid; module ≡-Reasoning)
import Relation.Binary.Reasoning.Preorder as PreorderReasoning
Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Relation/Ternary/Appending.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ open import Level using (Level; _⊔_)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
open import Data.Product as Prod using (∃₂; _×_; _,_; -,_)
open import Relation.Binary using (REL)
open import Relation.Binary.Core using (REL)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)

private
Expand Down
3 changes: 2 additions & 1 deletion src/Data/List/Relation/Ternary/Appending/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,8 @@ open import Data.List.Base using (List; [])
open import Data.List.Relation.Ternary.Appending
open import Data.List.Relation.Binary.Pointwise as Pw using (Pointwise; []; _∷_)
open import Level using (Level)
open import Relation.Binary using (REL; Rel; Trans)
open import Relation.Binary.Core using (REL; Rel)
open import Relation.Binary.Definitions using (Trans)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

private
Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Relation/Ternary/Appending/Setoid.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary using (Setoid)
open import Relation.Binary.Bundles using (Setoid)

module Data.List.Relation.Ternary.Appending.Setoid
{c ℓ} (S : Setoid c ℓ)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary using (Setoid)
open import Relation.Binary.Bundles using (Setoid)

module Data.List.Relation.Ternary.Appending.Setoid.Properties {c l} (S : Setoid c l) where

Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Relation/Ternary/Interleaving/Setoid.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary using (Setoid)
open import Relation.Binary.Bundles using (Setoid)

module Data.List.Relation.Ternary.Interleaving.Setoid {c ℓ} (S : Setoid c ℓ) where

Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary using (Setoid)
open import Relation.Binary.Bundles using (Setoid)

module Data.List.Relation.Ternary.Interleaving.Setoid.Properties
{c ℓ} (S : Setoid c ℓ) where
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Tree/AVL.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary using (StrictTotalOrder)
open import Relation.Binary.Bundles using (StrictTotalOrder)

module Data.Tree.AVL
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Trie/NonEmpty.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

{-# OPTIONS --cubical-compatible --sized-types #-}

open import Relation.Binary using (StrictTotalOrder)
open import Relation.Binary.Bundles using (StrictTotalOrder)

module Data.Trie.NonEmpty {k e r} (S : StrictTotalOrder k e r) where

Expand Down
2 changes: 1 addition & 1 deletion src/Data/Vec/Membership/DecPropositional.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary using (Decidable)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)

Expand Down
2 changes: 1 addition & 1 deletion src/Data/Vec/Relation/Binary/Equality/DecSetoid.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ open import Data.Nat.Base using (ℕ)
import Data.Vec.Relation.Binary.Equality.Setoid as Equality
import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
open import Level using (_⊔_)
open import Relation.Binary using (Decidable)
open import Relation.Binary.Definitions using (Decidable)

open DecSetoid DS

Expand Down
2 changes: 1 addition & 1 deletion src/Data/Vec/Relation/Unary/All/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ open import Level using (Level)
open import Function.Base using (_∘_; id)
open import Function.Inverse using (_↔_; inverse)
open import Relation.Unary using (Pred) renaming (_⊆_ to _⋐_)
open import Relation.Binary as B using (REL)
open import Relation.Binary.Core using (REL)
open import Relation.Binary.PropositionalEquality
using (_≡_; refl; cong; cong₂; →-to-⟶)

Expand Down
5 changes: 3 additions & 2 deletions src/Relation/Binary/Indexed/Homogeneous/Definitions.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,8 @@ module Relation.Binary.Indexed.Homogeneous.Definitions where

open import Data.Product using (_×_)
open import Level using (Level)
import Relation.Binary as B
open import Relation.Binary.Core using (_⇒_)
import Relation.Binary.Definitions as B
open import Relation.Unary.Indexed using (IPred)

open import Relation.Binary.Indexed.Homogeneous.Core
Expand All @@ -31,7 +32,7 @@ module _ (A : I → Set a) where
syntax Implies A _∼₁_ _∼₂_ = _∼₁_ ⇒[ A ] _∼₂_

Implies : IRel A ℓ₁ → IRel A ℓ₂ → Set _
Implies _∼₁_ _∼₂_ = ∀ {i} → _∼₁_ B.⇒ (_∼₂_ {i})
Implies _∼₁_ _∼₂_ = ∀ {i} → _∼₁_ ⇒ (_∼₂_ {i})

Reflexive : IRel A ℓ → Set _
Reflexive _∼_ = ∀ {i} → B.Reflexive (_∼_ {i})
Expand Down
3 changes: 2 additions & 1 deletion src/Relation/Nullary/Decidable.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,8 @@ open import Data.Sum.Base as Sum hiding (map)
open import Function.Base
open import Function.Bundles using
(Injection; module Injection; module Equivalence; _⇔_; _↔_; mk↔′)
open import Relation.Binary using (Setoid; module Setoid; Decidable)
open import Relation.Binary.Bundles using (Setoid; module Setoid)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Nullary.Reflects using (invert)
Expand Down