From 287678b132245a022e7e8530a3fec3ad12edf400 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Thu, 22 Jun 2023 13:28:15 -0400 Subject: [PATCH 1/2] Simplify more `Data.Product` import to `Data.Product.Base` --- src/Codata/Guarded/Stream/Properties.agda | 2 +- src/Codata/Guarded/Stream/Relation/Unary/All.agda | 2 +- src/Codata/Musical/Covec.agda | 2 +- src/Codata/Sized/Colist.agda | 2 +- src/Codata/Sized/Colist/Properties.agda | 2 +- src/Codata/Sized/M/Bisimilarity.agda | 2 +- src/Codata/Sized/M/Properties.agda | 2 +- src/Codata/Sized/Stream/Effectful.agda | 2 +- src/Codata/Sized/Stream/Properties.agda | 2 +- src/Data/AVL/IndexedMap.agda | 2 +- src/Data/Char/Properties.agda | 2 +- src/Data/Digit/Properties.agda | 2 +- src/Data/Fin/Induction.agda | 2 +- src/Data/Fin/Permutation.agda | 2 +- src/Data/Fin/Permutation/Components.agda | 2 +- src/Data/Fin/Permutation/Transposition/List.agda | 2 +- src/Data/Integer/Properties.agda | 3 +-- src/Data/List/Extrema/Core.agda | 2 +- src/Data/List/Extrema/Nat.agda | 2 +- src/Data/List/Fresh/Properties.agda | 2 +- src/Data/List/Fresh/Relation/Unary/All.agda | 2 +- src/Data/List/Fresh/Relation/Unary/All/Properties.agda | 2 +- src/Data/List/Fresh/Relation/Unary/Any/Properties.agda | 2 +- src/Data/List/Nary/NonDependent.agda | 2 +- src/Data/List/NonEmpty/Effectful.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/Strict.agda | 2 +- .../Relation/Binary/Permutation/Propositional/Properties.agda | 2 +- .../List/Relation/Binary/Prefix/Heterogeneous/Properties.agda | 2 +- 30 files changed, 30 insertions(+), 31 deletions(-) diff --git a/src/Codata/Guarded/Stream/Properties.agda b/src/Codata/Guarded/Stream/Properties.agda index 3e4bd83dcb..0a43417f7c 100644 --- a/src/Codata/Guarded/Stream/Properties.agda +++ b/src/Codata/Guarded/Stream/Properties.agda @@ -16,7 +16,7 @@ open import Data.List.Base as List using (List; []; _∷_) open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_) open import Data.Nat.Base using (ℕ; zero; suc; _+_; _*_) import Data.Nat.GeneralisedArithmetic as ℕ -open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂) +open import Data.Product.Base as Prod using (_×_; _,_; proj₁; proj₂) open import Data.Vec.Base as Vec using (Vec; _∷_) open import Function.Base using (const; flip; id; _∘′_; _$′_; _⟨_⟩_; _∘₂′_) open import Level using (Level) diff --git a/src/Codata/Guarded/Stream/Relation/Unary/All.agda b/src/Codata/Guarded/Stream/Relation/Unary/All.agda index ad87a7e589..69171a8960 100644 --- a/src/Codata/Guarded/Stream/Relation/Unary/All.agda +++ b/src/Codata/Guarded/Stream/Relation/Unary/All.agda @@ -9,7 +9,7 @@ module Codata.Guarded.Stream.Relation.Unary.All where open import Codata.Guarded.Stream using (Stream; head; tail) -open import Data.Product using (_,_; proj₁; proj₂) +open import Data.Product.Base using (_,_; proj₁; proj₂) open import Level open import Relation.Unary diff --git a/src/Codata/Musical/Covec.agda b/src/Codata/Musical/Covec.agda index 48cc1910e8..1d478ff610 100644 --- a/src/Codata/Musical/Covec.agda +++ b/src/Codata/Musical/Covec.agda @@ -14,7 +14,7 @@ open import Codata.Musical.Cofin using (Cofin; zero; suc) open import Codata.Musical.Colist as Colist using (Colist; []; _∷_) open import Data.Nat.Base using (ℕ; zero; suc) open import Data.Vec.Base using (Vec; []; _∷_) -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Function.Base using (_∋_) open import Level using (Level) open import Relation.Binary diff --git a/src/Codata/Sized/Colist.agda b/src/Codata/Sized/Colist.agda index 4f916fbc68..8ed85db5c9 100644 --- a/src/Codata/Sized/Colist.agda +++ b/src/Codata/Sized/Colist.agda @@ -12,7 +12,7 @@ open import Level using (Level) open import Size open import Data.Unit.Base open import Data.Nat.Base -open import Data.Product using (_×_ ; _,_) +open import Data.Product.Base using (_×_ ; _,_) open import Data.These.Base using (These; this; that; these) open import Data.Maybe.Base using (Maybe; nothing; just) open import Data.List.Base using (List; []; _∷_) diff --git a/src/Codata/Sized/Colist/Properties.agda b/src/Codata/Sized/Colist/Properties.agda index dea697b088..a3b0dc469e 100644 --- a/src/Codata/Sized/Colist/Properties.agda +++ b/src/Codata/Sized/Colist/Properties.agda @@ -27,7 +27,7 @@ open import Data.Maybe.Base as Maybe using (Maybe; nothing; just) import Data.Maybe.Properties as Maybeₚ open import Data.Maybe.Relation.Unary.All using (All; nothing; just) open import Data.Nat.Base as ℕ using (zero; suc; z≤n; s≤s) -open import Data.Product as Prod using (_×_; _,_; uncurry) +open import Data.Product.Base as Prod using (_×_; _,_; uncurry) open import Data.These.Base as These using (These; this; that; these) open import Data.Vec.Base as Vec using (Vec; []; _∷_) open import Function.Base diff --git a/src/Codata/Sized/M/Bisimilarity.agda b/src/Codata/Sized/M/Bisimilarity.agda index 1b8cbd3188..75450da7f1 100644 --- a/src/Codata/Sized/M/Bisimilarity.agda +++ b/src/Codata/Sized/M/Bisimilarity.agda @@ -14,7 +14,7 @@ open import Codata.Sized.Thunk open import Codata.Sized.M open import Data.Container.Core open import Data.Container.Relation.Binary.Pointwise using (Pointwise; _,_) -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Function.Base using (_∋_) open import Relation.Binary import Relation.Binary.PropositionalEquality as P diff --git a/src/Codata/Sized/M/Properties.agda b/src/Codata/Sized/M/Properties.agda index 3b26955e60..a346a4d8d8 100644 --- a/src/Codata/Sized/M/Properties.agda +++ b/src/Codata/Sized/M/Properties.agda @@ -15,7 +15,7 @@ open import Codata.Sized.M open import Codata.Sized.M.Bisimilarity open import Data.Container.Core as C hiding (map) import Data.Container.Morphism as Mp -open import Data.Product as Prod using (_,_) +open import Data.Product.Base as Prod using (_,_) open import Data.Product.Properties hiding (map-cong) open import Function.Base using (_$′_; _∘′_) import Relation.Binary.PropositionalEquality as P diff --git a/src/Codata/Sized/Stream/Effectful.agda b/src/Codata/Sized/Stream/Effectful.agda index 00fe7eb2b1..a9636ad027 100644 --- a/src/Codata/Sized/Stream/Effectful.agda +++ b/src/Codata/Sized/Stream/Effectful.agda @@ -8,7 +8,7 @@ module Codata.Sized.Stream.Effectful where -open import Data.Product using (<_,_>) +open import Data.Product.Base using (<_,_>) open import Codata.Sized.Stream open import Effect.Functor open import Effect.Applicative diff --git a/src/Codata/Sized/Stream/Properties.agda b/src/Codata/Sized/Stream/Properties.agda index 539a6b7b20..2c4ac9160e 100644 --- a/src/Codata/Sized/Stream/Properties.agda +++ b/src/Codata/Sized/Stream/Properties.agda @@ -20,7 +20,7 @@ open import Data.Nat.GeneralisedArithmetic using (fold; fold-pull) open import Data.List.Base as List using ([]; _∷_) open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_) import Data.List.Relation.Binary.Equality.Propositional as Eq -open import Data.Product as Prod using (_,_) +open import Data.Product.Base as Prod using (_,_) open import Data.Vec.Base as Vec using (_∷_) open import Function.Base using (id; _$_; _∘′_; const) diff --git a/src/Data/AVL/IndexedMap.agda b/src/Data/AVL/IndexedMap.agda index 64a0d5c36a..f7bad24033 100644 --- a/src/Data/AVL/IndexedMap.agda +++ b/src/Data/AVL/IndexedMap.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Data.Product as Prod +open import Data.Product open import Relation.Binary open import Relation.Binary.PropositionalEquality using (_≡_; cong; subst) import Data.Tree.AVL.Value diff --git a/src/Data/Char/Properties.agda b/src/Data/Char/Properties.agda index 1db34c4f0b..6dff8a589f 100644 --- a/src/Data/Char/Properties.agda +++ b/src/Data/Char/Properties.agda @@ -12,7 +12,7 @@ open import Data.Bool.Base using (Bool) open import Data.Char.Base import Data.Nat.Base as ℕ import Data.Nat.Properties as ℕₚ -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Function.Base open import Relation.Nullary using (¬_; yes; no) diff --git a/src/Data/Digit/Properties.agda b/src/Data/Digit/Properties.agda index 355467ec39..51a5060ace 100644 --- a/src/Data/Digit/Properties.agda +++ b/src/Data/Digit/Properties.agda @@ -11,7 +11,7 @@ import Data.Char.Properties as Charₚ open import Data.Nat.Base using (ℕ) open import Data.Nat.Properties using (_≤?_) open import Data.Fin.Properties using (inject≤-injective) -open import Data.Product using (_,_; proj₁) +open import Data.Product.Base using (_,_; proj₁) open import Data.Vec.Relation.Unary.Unique.Propositional using (Unique) import Data.Vec.Relation.Unary.Unique.Propositional.Properties as Uniqueₚ open import Data.Vec.Relation.Unary.AllPairs using (allPairs?) diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda index 3c9bf54546..b0cf553d0d 100644 --- a/src/Data/Fin/Induction.agda +++ b/src/Data/Fin/Induction.agda @@ -13,7 +13,7 @@ open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _∸_; s≤s) open import Data.Nat.Properties using (n<1+n; ≤⇒≯) import Data.Nat.Induction as ℕ import Data.Nat.Properties as ℕ -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Data.Vec.Base as Vec using (Vec; []; _∷_) open import Data.Vec.Relation.Unary.Linked as Linked using (Linked; [-]; _∷_) import Data.Vec.Relation.Unary.Linked.Properties as Linkedₚ diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda index f6a7820b52..852a609779 100644 --- a/src/Data/Fin/Permutation.agda +++ b/src/Data/Fin/Permutation.agda @@ -15,7 +15,7 @@ open import Data.Fin.Patterns open import Data.Fin.Properties import Data.Fin.Permutation.Components as PC open import Data.Nat.Base using (ℕ; suc; zero) -open import Data.Product using (_,_; proj₂) +open import Data.Product.Base using (_,_; proj₂) open import Function.Bundles using (_↔_; Injection; Inverse; mk↔′) open import Function.Construct.Composition using (_↔-∘_) open import Function.Construct.Identity using (↔-id) diff --git a/src/Data/Fin/Permutation/Components.agda b/src/Data/Fin/Permutation/Components.agda index b053cee86b..e75fa29eb2 100644 --- a/src/Data/Fin/Permutation/Components.agda +++ b/src/Data/Fin/Permutation/Components.agda @@ -13,7 +13,7 @@ open import Data.Fin.Base open import Data.Fin.Properties open import Data.Nat.Base as ℕ using (zero; suc; _∸_) import Data.Nat.Properties as ℕₚ -open import Data.Product using (proj₂) +open import Data.Product.Base using (proj₂) open import Function.Base using (_∘_) open import Relation.Nullary.Reflects using (invert) open import Relation.Nullary using (does; _because_; yes; no) diff --git a/src/Data/Fin/Permutation/Transposition/List.agda b/src/Data/Fin/Permutation/Transposition/List.agda index 07feee0020..4da8f08d37 100644 --- a/src/Data/Fin/Permutation/Transposition/List.agda +++ b/src/Data/Fin/Permutation/Transposition/List.agda @@ -14,7 +14,7 @@ open import Data.Fin.Permutation as P hiding (lift₀) import Data.Fin.Permutation.Components as PC open import Data.List.Base using (List; []; _∷_; map) open import Data.Nat.Base using (ℕ; suc; zero) -open import Data.Product using (_×_; _,_) +open import Data.Product.Base using (_×_; _,_) open import Function.Base using (_∘_) open import Relation.Binary.PropositionalEquality using (_≡_; sym; cong; module ≡-Reasoning) diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 518c1456f4..78011e54b1 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -21,11 +21,10 @@ open import Data.Nat as ℕ hiding (module ℕ) import Data.Nat.Properties as ℕ open import Data.Nat.Solver -open import Data.Product using (proj₁; proj₂; _,_) +open import Data.Product.Base using (proj₁; proj₂; _,_; _×_) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′) open import Data.Sign as Sign using (Sign) renaming (_*_ to _𝕊*_) import Data.Sign.Properties as 𝕊ₚ -open import Data.Product using (_×_) open import Function.Base using (_∘_; _$_; id) open import Level using (0ℓ) open import Relation.Binary diff --git a/src/Data/List/Extrema/Core.agda b/src/Data/List/Extrema/Core.agda index aa0b3f8da9..08e86b544d 100644 --- a/src/Data/List/Extrema/Core.agda +++ b/src/Data/List/Extrema/Core.agda @@ -15,7 +15,7 @@ open import Algebra.Core open import Algebra.Definitions import Algebra.Construct.NaturalChoice.Min as Min import Algebra.Construct.NaturalChoice.Max as Max -open import Data.Product using (_×_; _,_) +open import Data.Product.Base using (_×_; _,_) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Level using (Level) open import Relation.Binary.PropositionalEquality using (_≡_) diff --git a/src/Data/List/Extrema/Nat.agda b/src/Data/List/Extrema/Nat.agda index d1d8f3f4ac..5944615be4 100644 --- a/src/Data/List/Extrema/Nat.agda +++ b/src/Data/List/Extrema/Nat.agda @@ -18,7 +18,7 @@ open import Data.List.Base using (List) import Data.List.Extrema open import Data.List.Relation.Unary.Any as Any using (Any) open import Data.List.Relation.Unary.All as All using (All) -open import Data.Product using (_×_; _,_; uncurry′) +open import Data.Product.Base using (_×_; _,_; uncurry′) open import Level using (Level) open import Relation.Binary.PropositionalEquality using (_≢_) diff --git a/src/Data/List/Fresh/Properties.agda b/src/Data/List/Fresh/Properties.agda index cc8925eca6..b22347f92e 100644 --- a/src/Data/List/Fresh/Properties.agda +++ b/src/Data/List/Fresh/Properties.agda @@ -9,7 +9,7 @@ module Data.List.Fresh.Properties where open import Level using (Level; _⊔_; Lift) -open import Data.Product using (_,_) +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) diff --git a/src/Data/List/Fresh/Relation/Unary/All.agda b/src/Data/List/Fresh/Relation/Unary/All.agda index c013f934bb..b0e2115ce1 100644 --- a/src/Data/List/Fresh/Relation/Unary/All.agda +++ b/src/Data/List/Fresh/Relation/Unary/All.agda @@ -9,7 +9,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.Product.Base using (_×_; _,_; proj₁; uncurry) open import Data.Sum.Base as Sum using (inj₁; inj₂) open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_) open import Relation.Unary as U diff --git a/src/Data/List/Fresh/Relation/Unary/All/Properties.agda b/src/Data/List/Fresh/Relation/Unary/All/Properties.agda index cbad777b96..9a90ad28df 100644 --- a/src/Data/List/Fresh/Relation/Unary/All/Properties.agda +++ b/src/Data/List/Fresh/Relation/Unary/All/Properties.agda @@ -11,7 +11,7 @@ module Data.List.Fresh.Relation.Unary.All.Properties where open import Level using (Level; _⊔_; Lift) open import Data.Empty open import Data.Nat.Base using (ℕ; zero; suc) -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Function.Base using (_∘′_) open import Relation.Nullary open import Relation.Unary as U diff --git a/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda b/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda index f185a2ef32..6dcc04dc4a 100644 --- a/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda +++ b/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda @@ -12,7 +12,7 @@ open import Level using (Level; _⊔_; Lift) open import Data.Bool.Base using (true; false) open import Data.Empty open import Data.Nat.Base using (ℕ; zero; suc) -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂) open import Function.Base using (_∘′_) open import Relation.Nullary.Reflects using (invert) diff --git a/src/Data/List/Nary/NonDependent.agda b/src/Data/List/Nary/NonDependent.agda index 6fff2b0dac..f95da6345c 100644 --- a/src/Data/List/Nary/NonDependent.agda +++ b/src/Data/List/Nary/NonDependent.agda @@ -10,7 +10,7 @@ module Data.List.Nary.NonDependent where open import Data.Nat.Base using (zero; suc) open import Data.List.Base as List using (List; []; _∷_) -open import Data.Product as Prod using (_,_) +open import Data.Product.Base as Prod using (_,_) open import Data.Product.Nary.NonDependent using (Product) open import Function.Base using () open import Function.Nary.NonDependent.Base diff --git a/src/Data/List/NonEmpty/Effectful.agda b/src/Data/List/NonEmpty/Effectful.agda index 654002c839..5b37642808 100644 --- a/src/Data/List/NonEmpty/Effectful.agda +++ b/src/Data/List/NonEmpty/Effectful.agda @@ -11,7 +11,7 @@ module Data.List.NonEmpty.Effectful where open import Agda.Builtin.List import Data.List.Effectful as List open import Data.List.NonEmpty.Base -open import Data.Product using (uncurry) +open import Data.Product.Base using (uncurry) open import Effect.Functor open import Effect.Applicative open import Effect.Monad diff --git a/src/Data/List/Relation/Binary/Disjoint/Setoid.agda b/src/Data/List/Relation/Binary/Disjoint/Setoid.agda index d5003aab4e..6ea7e15cf7 100644 --- a/src/Data/List/Relation/Binary/Disjoint/Setoid.agda +++ b/src/Data/List/Relation/Binary/Disjoint/Setoid.agda @@ -15,7 +15,7 @@ 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) -open import Data.Product using (_×_; _,_) +open import Data.Product.Base using (_×_; _,_) open Setoid S renaming (Carrier to A) open import Data.List.Membership.Setoid S using (_∈_; _∉_) diff --git a/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda index 3f0701a8ef..43a67d4d7d 100644 --- a/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda @@ -14,7 +14,7 @@ import Data.List.Relation.Unary.Any as Any open import Data.List.Relation.Unary.All as All open import Data.List.Relation.Unary.All.Properties using (¬Any⇒All¬) open import Data.List.Relation.Unary.Any.Properties using (++⁻) -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Data.Sum.Base using (inj₁; inj₂) open import Relation.Binary open import Relation.Nullary.Negation using (¬_) diff --git a/src/Data/List/Relation/Binary/Lex/Strict.agda b/src/Data/List/Relation/Binary/Lex/Strict.agda index fef11ad07e..c0428b347d 100644 --- a/src/Data/List/Relation/Binary/Lex/Strict.agda +++ b/src/Data/List/Relation/Binary/Lex/Strict.agda @@ -14,7 +14,7 @@ module Data.List.Relation.Binary.Lex.Strict where open import Data.Empty using (⊥) open import Data.Unit.Base using (⊤; tt) open import Function.Base using (_∘_; id) -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Data.Sum.Base using (inj₁; inj₂) open import Data.List.Base using (List; []; _∷_) open import Level using (_⊔_) diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda index f5a87cb067..d4329fe153 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda @@ -13,7 +13,7 @@ open import Algebra.Definitions open import Algebra.Structures open import Data.Bool.Base using (Bool; true; false) open import Data.Nat using (suc) -open import Data.Product using (-,_; proj₂) +open import Data.Product.Base using (-,_; proj₂) open import Data.List.Base as List open import Data.List.Relation.Binary.Permutation.Propositional open import Data.List.Relation.Unary.Any using (Any; here; there) diff --git a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda index eea13df3b6..fd0cfb22a0 100644 --- a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda @@ -19,7 +19,7 @@ open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_) open import Data.List.Relation.Binary.Prefix.Heterogeneous as Prefix hiding (PrefixView; _++_) 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 Data.Product.Base as Prod using (_×_; _,_; proj₁; proj₂; uncurry) open import Function.Base open import Relation.Nullary.Negation using (¬_) From 1816b6ee015cb006552bd037ae85312855ca9c59 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Sun, 2 Jul 2023 23:39:59 -0400 Subject: [PATCH 2/2] Missed an import --- src/Data/AVL/IndexedMap.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/AVL/IndexedMap.agda b/src/Data/AVL/IndexedMap.agda index f7bad24033..ce67d16a28 100644 --- a/src/Data/AVL/IndexedMap.agda +++ b/src/Data/AVL/IndexedMap.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Data.Product +open import Data.Product.Base using (∃) open import Relation.Binary open import Relation.Binary.PropositionalEquality using (_≡_; cong; subst) import Data.Tree.AVL.Value