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

More simplifications for Relation.Binary imports #2038

Merged
merged 4 commits into from
Aug 11, 2023
Merged

More simplifications for Relation.Binary imports #2038

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
4e1d237
More simplifications for `Relation.Binary` imports
Saransh-cpp Jun 26, 2023
3b6a8a3
Resolve conflicts
Saransh-cpp Jul 29, 2023
55c6293
More simplifications for `Relation.Binary` imports
Saransh-cpp Jun 25, 2023
5776c7c
spaces
Saransh-cpp Jul 30, 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 README/Nary.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ open import Data.Product using (_×_; _,_)
open import Data.Sum.Base using (inj₁; inj₂)
open import Function.Base using (id; flip; _∘′_)
open import Relation.Nullary
open import Relation.Binary using (module Tri); open Tri
open import Relation.Binary.Definitions using (module Tri); open Tri
open import Relation.Binary.PropositionalEquality

private
Expand Down
2 changes: 1 addition & 1 deletion src/Data/AVL.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
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/AVL/Indexed.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.Indexed
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) where
Expand Down
4 changes: 3 additions & 1 deletion src/Data/AVL/NonEmpty/Propositional.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,9 @@

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

open import Relation.Binary using (Rel; IsStrictTotalOrder; StrictTotalOrder)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Structures using (IsStrictTotalOrder)
open import Relation.Binary.Bundles using (StrictTotalOrder)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)

module Data.AVL.NonEmpty.Propositional
Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Extrema.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 (TotalOrder; Setoid)
open import Relation.Binary.Bundles using (TotalOrder; Setoid)

module Data.List.Extrema
{b ℓ₁ ℓ₂} (totalOrder : TotalOrder b ℓ₁ ℓ₂) where
Expand Down
3 changes: 2 additions & 1 deletion src/Data/List/Fresh/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 Level using (Level; _⊔_; Lift)
open import Data.Product.Base using (_,_)
open import Relation.Nullary
open import Relation.Unary as U using (Pred)
open import Relation.Binary as B using (Rel)
import Relation.Binary.Definitions as B
open import Relation.Binary.Core using (Rel)

open import Data.List.Fresh

Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/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 using (_≡_)
open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)

Expand Down
3 changes: 2 additions & 1 deletion src/Data/List/Membership/DecSetoid.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 (Decidable; DecSetoid)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.Bundles using (DecSetoid)
open import Relation.Nullary.Decidable using (¬?)

module Data.List.Membership.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where
Expand Down
4 changes: 2 additions & 2 deletions src/Data/List/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,10 +34,10 @@ open import Data.Fin.Properties using (toℕ-cast)
open import Function.Base using (id; _∘_; _∘′_; _∋_; _-⟨_∣; ∣_⟩-_; _$_; const; flip)
open import Function.Definitions using (Injective)
open import Level using (Level)
open import Relation.Binary as B using (DecidableEquality)
open import Relation.Binary.Definitions as B using (DecidableEquality)
import Relation.Binary.Reasoning.Setoid as EqR
open import Relation.Binary.PropositionalEquality as P hiding ([_])
open import Relation.Binary as B using (Rel)
open import Relation.Binary.Core using (Rel)
open import Relation.Nullary.Reflects using (invert)
open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no; contradiction)
open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋; ¬?; _×-dec_)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Relation/Binary/Equality/DecSetoid.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ module Data.List.Relation.Binary.Equality.DecSetoid
import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
import Data.List.Relation.Binary.Pointwise as PW
open import Level
open import Relation.Binary using (Decidable)
open import Relation.Binary.Definitions using (Decidable)
open DecSetoid DS

------------------------------------------------------------------------
Expand Down
6 changes: 4 additions & 2 deletions src/Data/List/Relation/Binary/Equality/Setoid.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,9 @@
{-# OPTIONS --cubical-compatible --safe #-}

open import Algebra.Core using (Op₂)
open import Relation.Binary using (Setoid)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Definitions using (Transitive; Symmetric; Reflexive; _Respects_)
open import Relation.Binary.Structures using (IsEquivalence)

module Data.List.Relation.Binary.Equality.Setoid {a ℓ} (S : Setoid a ℓ) where

Expand All @@ -17,7 +19,7 @@ open import Data.List.Relation.Binary.Pointwise as PW using (Pointwise)
open import Data.List.Relation.Unary.Unique.Setoid S using (Unique)
open import Function.Base using (_∘_)
open import Level
open import Relation.Binary renaming (Rel to Rel₂)
open import Relation.Binary.Core renaming (Rel to Rel₂)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Binary.Properties.Setoid S using (≉-resp₂)
open import Relation.Unary as U using (Pred)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Relation/Binary/Infix/Heterogeneous.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
module Data.List.Relation.Binary.Infix.Heterogeneous where

open import Level
open import Relation.Binary using (REL; _⇒_)
open import Relation.Binary.Core using (REL; _⇒_)
open import Data.List.Base as List using (List; []; _∷_; _++_)
open import Data.List.Relation.Binary.Pointwise
using (Pointwise)
Expand Down
3 changes: 2 additions & 1 deletion src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,8 @@ open import Function.Base using (case_of_; _$′_)
open import Relation.Nullary.Decidable using (yes; no; does; map′; _⊎-dec_)
open import Relation.Nullary.Negation using (¬_; contradiction)
open import Relation.Unary as U using (Pred)
open import Relation.Binary using (REL; _⇒_; Decidable; Trans; Antisym)
open import Relation.Binary.Core using (REL; _⇒_)
open import Relation.Binary.Definitions using (Decidable; Trans; Antisym)
open import Relation.Binary.PropositionalEquality.Core using (_≢_; refl; cong)
open import Data.List.Relation.Binary.Pointwise.Base as Pointwise using (Pointwise)
open import Data.List.Relation.Binary.Infix.Heterogeneous
Expand Down
5 changes: 4 additions & 1 deletion src/Data/List/Relation/Binary/Pointwise.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,10 @@ open import Level
open import Relation.Nullary hiding (Irrelevant)
import Relation.Nullary.Decidable as Dec using (map′)
open import Relation.Unary as U using (Pred)
open import Relation.Binary renaming (Rel to Rel₂)
open import Relation.Binary.Core renaming (Rel to Rel₂)
open import Relation.Binary.Definitions using (_Respects_; _Respects₂_)
open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder; Poset)
open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence; IsPartialOrder; IsPreorder)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
import Relation.Binary.PropositionalEquality.Properties as P

Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ import Data.List.Relation.Binary.Sublist.Setoid.Properties
open import Data.Product using (∃; _,_; proj₂)
open import Function.Base
open import Level using (Level)
open import Relation.Binary using (_Respects_)
open import Relation.Binary.Definitions using (_Respects_)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary using (Pred)

Expand Down
5 changes: 3 additions & 2 deletions src/Data/List/Relation/Binary/Sublist/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; _⇒_; _Preserves_⟶_)
open import Relation.Binary.Core using (Rel; _⇒_; _Preserves_⟶_)
open import Relation.Binary.Bundles using (Setoid)

module Data.List.Relation.Binary.Sublist.Setoid.Properties
{c ℓ} (S : Setoid c ℓ) where
Expand All @@ -20,7 +21,7 @@ open import Data.Product using (∃; _,_; proj₂)
open import Function.Base
open import Function.Bundles using (_⇔_; _⤖_)
open import Level
open import Relation.Binary using () renaming (Decidable to Decidable₂)
open import Relation.Binary.Definitions using () renaming (Decidable to Decidable₂)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
open import Relation.Binary.Structures using (IsDecTotalOrder)
open import Relation.Unary using (Pred; Decidable; Irrelevant)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
module Data.List.Relation.Binary.Suffix.Heterogeneous where

open import Level
open import Relation.Binary using (REL; _⇒_)
open import Relation.Binary.Core using (REL; _⇒_)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.Relation.Binary.Pointwise.Base as Pointwise
using (Pointwise; []; _∷_)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Relation/Unary/AllPairs/Core.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@

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

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

module Data.List.Relation.Unary.AllPairs.Core
{a ℓ} {A : Set a} (R : Rel A ℓ) where
Expand Down
3 changes: 2 additions & 1 deletion src/Data/List/Relation/Unary/AllPairs/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,8 @@ open import Data.Nat.Base using (zero; suc; _<_; z≤n; s≤s)
open import Data.Nat.Properties using (≤-refl; m<n⇒m<1+n)
open import Function.Base using (_∘_; flip)
open import Level using (Level)
open import Relation.Binary using (Rel; DecSetoid)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (DecSetoid)
open import Relation.Binary.PropositionalEquality.Core using (_≢_)
open import Relation.Unary using (Pred; Decidable)
open import Relation.Nullary.Decidable using (does)
Expand Down
3 changes: 2 additions & 1 deletion src/Data/List/Relation/Unary/Grouped/Properties.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.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _
open import Data.List.Relation.Unary.Grouped
open import Function.Base using (_∘_)
open import Function.Bundles using (module Equivalence; _⇔_)
open import Relation.Binary as B using (REL; Rel)
open import Relation.Binary.Definitions as B
open import Relation.Binary.Core using (REL; Rel)
open import Relation.Unary as U using (Pred)
open import Relation.Nullary using (¬_; does; yes; no)
open import Relation.Nullary.Negation using (contradiction)
Expand Down
3 changes: 2 additions & 1 deletion src/Data/List/Relation/Unary/Linked.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.Maybe.Relation.Binary.Connected
using (Connected; just; just-nothing)
open import Function.Base using (id; _∘_)
open import Level using (Level; _⊔_)
open import Relation.Binary as B using (Rel; _⇒_)
open import Relation.Binary.Definitions as B
open import Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Sort.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
{-# OPTIONS --cubical-compatible --safe #-}

open import Data.List.Base using (List)
open import Relation.Binary using (DecTotalOrder)
open import Relation.Binary.Bundles using (DecTotalOrder)

module Data.List.Sort
{a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Sort/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
open import Data.List.Base using (List)
open import Data.List.Relation.Binary.Permutation.Propositional
open import Level using (_⊔_)
open import Relation.Binary using (TotalOrder)
open import Relation.Binary.Bundles using (TotalOrder)

module Data.List.Sort.Base
{a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/List/Sort/MergeSort.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ open import Data.Nat.Induction
open import Data.Nat.Properties using (m<n⇒m<1+n)
open import Data.Product as Prod using (_,_)
open import Function.Base using (_∘_)
open import Relation.Binary using (DecTotalOrder)
open import Relation.Binary.Bundles using (DecTotalOrder)
open import Relation.Nullary.Negation using (¬_)

module Data.List.Sort.MergeSort
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Maybe/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ open import Data.Product using (_,_)
open import Function.Base using (_∋_; id; _∘_; _∘′_)
open import Function.Definitions using (Injective)
open import Level using (Level)
open import Relation.Binary using (Decidable)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable using (yes; no)
open import Relation.Nullary.Decidable using (map′)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Nat/Divisibility/Core.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ open import Data.Nat.Base using (ℕ; _*_)
open import Data.Nat.Properties
open import Level using (0ℓ)
open import Relation.Nullary.Negation using (¬_)
open import Relation.Binary using (Rel)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality
using (_≡_; refl; sym; cong₂; module ≡-Reasoning)

Expand Down
2 changes: 1 addition & 1 deletion src/Data/Product/Effectful/Examples.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ open import Data.Product
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Function.Base using (id)
import Function.Identity.Effectful as Id
open import Relation.Binary using (Rel)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

------------------------------------------------------------------------
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Product/Properties.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.Base
open import Function.Base using (_∋_; _∘_; id)
open import Function.Bundles using (_↔_; mk↔′)
open import Level using (Level)
open import Relation.Binary using (DecidableEquality)
open import Relation.Binary.Definitions using (DecidableEquality)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable as Dec using (Dec; yes; no)

Expand Down
2 changes: 1 addition & 1 deletion src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.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
open import Data.Product.Relation.Binary.Pointwise.Dependent
open import Function.Base
open import Function.Inverse using (Inverse)
open import Relation.Binary using (_⇒_)
open import Relation.Binary.Core using (_⇒_)
open import Relation.Binary.HeterogeneousEquality as H using (_≅_)
open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Sum/Properties.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
open import Data.Sum.Base
open import Function.Base using (_∋_; _∘_; id)
open import Function.Bundles using (mk↔′; _↔_)
open import Relation.Binary using (Decidable)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable using (yes; no)
open import Relation.Nullary.Decidable using (map′)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/These/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.These.Properties where
open import Data.Product
open import Data.These.Base
open import Function.Base using (_∘_)
open import Relation.Binary using (Decidable)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable using (yes; no; map′; _×-dec_)

Expand Down
4 changes: 2 additions & 2 deletions src/Data/Tree/AVL/Indexed.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.Tree.AVL.Indexed
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) where
Expand All @@ -19,7 +19,7 @@ open import Data.List.Base as List using (List)
open import Data.DifferenceList using (DiffList; []; _∷_; _++_)
open import Function.Base as F hiding (const)
open import Relation.Unary
open import Relation.Binary using (_Respects_; Tri; tri<; tri≈; tri>)
open import Relation.Binary.Definitions using (_Respects_; Tri; tri<; tri≈; tri>)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

private
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Tree/AVL/Indexed/Relation/Unary/All.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.Tree.AVL.Indexed.Relation.Unary.All
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Tree/AVL/Indexed/Relation/Unary/Any.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.Tree.AVL.Indexed.Relation.Unary.Any
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
Expand Down
4 changes: 2 additions & 2 deletions src/Data/Tree/AVL/Indexed/Relation/Unary/Any/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 (StrictTotalOrder)
open import Relation.Binary.Bundles using (StrictTotalOrder)

module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties
{a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
Expand All @@ -21,7 +21,7 @@ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
open import Function.Base as F
open import Level using (Level)

open import Relation.Binary using (_Respects_; tri<; tri≈; tri>)
open import Relation.Binary.Definitions using (_Respects_; tri<; tri≈; tri>)
open import Relation.Binary.PropositionalEquality.Core using (_≡_) renaming (refl to ≡-refl)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Negation using (contradiction)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Tree/AVL/Map.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@

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

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

module Data.Tree.AVL.Map
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
Expand Down
4 changes: 2 additions & 2 deletions src/Data/Tree/AVL/Map/Membership/Propositional.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 (StrictTotalOrder)
open import Relation.Binary.Bundles using (StrictTotalOrder)

module Data.Tree.AVL.Map.Membership.Propositional
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
Expand All @@ -21,7 +21,7 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Function.Base using (_∘_; _∘′_)
open import Level using (Level)

open import Relation.Binary using (Transitive; Symmetric; _Respectsˡ_)
open import Relation.Binary.Definitions using (Transitive; Symmetric; _Respectsˡ_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Construct.Intersection using (_∩_)
open import Relation.Binary.PropositionalEquality
Expand Down
Loading