From e5b04e95d3465f51a75c0058b53973cab0c0619f Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Sun, 2 Jul 2023 23:33:29 -0400 Subject: [PATCH 1/5] Final `Data.Product` imports simplified --- README/Case.agda | 1 - README/Data/Container/Indexed.agda | 2 +- README/Data/Integer.agda | 1 - README/Data/List/Fresh.agda | 2 +- README/Data/Record.agda | 2 +- README/Data/Wrap.agda | 2 +- README/Design/Decidability.agda | 2 +- README/Foreign/Haskell.agda | 2 +- README/Inspect.agda | 2 +- README/Relation/Binary/TypeClasses.agda | 2 +- README/Text/Pretty.agda | 2 +- src/Algebra/Construct/DirectProduct.agda | 2 +- src/Algebra/Construct/LexProduct.agda | 2 +- src/Algebra/Lattice/Construct/DirectProduct.agda | 2 +- src/Algebra/Module/Construct/DirectProduct.agda | 2 +- src/Algebra/Module/Definitions/Left.agda | 1 - src/Algebra/Module/Definitions/Right.agda | 1 - src/Algebra/Module/Morphism/ModuleHomomorphism.agda | 2 +- src/Algebra/Morphism/Construct/Composition.agda | 1 - src/Algebra/Morphism/GroupMonomorphism.agda | 2 +- src/Algebra/Morphism/MagmaMonomorphism.agda | 2 +- src/Algebra/Morphism/RingMonomorphism.agda | 2 +- src/Algebra/Properties/Loop.agda | 1 - src/Algebra/Properties/MiddleBolLoop.agda | 1 - src/Algebra/Properties/MoufangLoop.agda | 2 +- src/Algebra/Properties/Quasigroup.agda | 2 +- src/Algebra/Solver/Monoid.agda | 2 +- src/Codata/Musical/Conversion.agda | 2 +- src/Codata/Musical/M/Indexed.agda | 2 +- src/Data/AVL/IndexedMap.agda | 2 +- src/Data/Container/Indexed/Core.agda | 2 +- src/Data/Container/Indexed/FreeMonad.agda | 2 +- src/Data/Integer/GCD.agda | 2 +- src/Data/List/Countdown.agda | 2 +- src/Data/List/Relation/Binary/Lex/NonStrict.agda | 1 - .../List/Relation/Binary/Sublist/Heterogeneous/Solver.agda | 2 +- src/Data/Maybe/Relation/Binary/Connected.agda | 1 - src/Data/Maybe/Relation/Binary/Pointwise.agda | 2 +- src/Data/Nat/GCD.agda | 3 ++- src/Data/Nat/LCM.agda | 2 +- src/Data/Nat/Primality.agda | 2 +- src/Data/Product/Effectful/Examples.agda | 2 +- src/Data/Product/Function/Dependent/Propositional.agda | 2 +- src/Data/Product/Function/Dependent/Propositional/WithK.agda | 2 +- src/Data/Product/Function/Dependent/Setoid.agda | 2 +- src/Data/Product/Function/Dependent/Setoid/WithK.agda | 2 +- src/Data/Product/Function/NonDependent/Propositional.agda | 2 +- src/Data/Product/Function/NonDependent/Setoid.agda | 2 +- src/Data/Product/Properties/WithK.agda | 2 +- .../Product/Relation/Binary/Pointwise/Dependent/WithK.agda | 2 +- src/Data/Sum/Relation/Binary/LeftOrder.agda | 2 +- src/Data/These/Properties.agda | 2 +- src/Data/Tree/AVL/Indexed/WithK.agda | 1 - src/Data/Tree/AVL/Key.agda | 2 +- src/Data/Universe.agda | 1 - src/Data/Universe/Indexed.agda | 2 +- src/Data/W/Indexed.agda | 2 +- src/Data/W/WithK.agda | 2 +- src/Effect/Applicative/Predicate.agda | 2 +- src/Effect/Monad/Predicate.agda | 2 +- src/Effect/Monad/State.agda | 2 +- src/Effect/Monad/State/Indexed.agda | 2 +- src/Function/Bijection.agda | 1 - src/Function/Endomorphism/Setoid.agda | 2 +- src/Function/LeftInverse.agda | 1 - src/Function/Properties/RightInverse.agda | 2 +- src/Function/Properties/Surjection.agda | 2 +- src/Function/Surjection.agda | 1 - src/Induction/Lexicographic.agda | 2 +- src/Relation/Binary/Construct/Add/Infimum/Strict.agda | 2 +- src/Relation/Binary/Construct/Add/Supremum/Strict.agda | 2 +- src/Relation/Binary/Construct/Composition.agda | 2 +- src/Relation/Binary/Construct/Flip/Ord.agda | 2 +- src/Relation/Binary/Construct/FromPred.agda | 1 - src/Relation/Binary/Construct/FromRel.agda | 1 - src/Relation/Binary/Construct/On.agda | 2 +- src/Relation/Binary/HeterogeneousEquality.agda | 1 - .../Binary/HeterogeneousEquality/Quotients/Examples.agda | 2 +- .../Binary/Lattice/Properties/BoundedJoinSemilattice.agda | 2 +- .../Binary/Lattice/Properties/BoundedMeetSemilattice.agda | 1 - src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda | 2 +- src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda | 1 - src/Relation/Unary/PredicateTransformer.agda | 2 +- src/Tactic/Cong.agda | 2 +- src/Tactic/RingSolver/NonReflective.agda | 2 +- src/Text/Format/Generic.agda | 2 +- 86 files changed, 68 insertions(+), 86 deletions(-) diff --git a/README/Case.agda b/README/Case.agda index 358460a63b..d088d78b6b 100644 --- a/README/Case.agda +++ b/README/Case.agda @@ -14,7 +14,6 @@ open import Data.Maybe hiding (from-just) open import Data.Nat hiding (pred) open import Data.List open import Data.Sum -open import Data.Product open import Function.Base using (case_of_; case_return_of_) open import Relation.Nullary open import Relation.Binary diff --git a/README/Data/Container/Indexed.agda b/README/Data/Container/Indexed.agda index 0c94e182ec..63a782f8de 100644 --- a/README/Data/Container/Indexed.agda +++ b/README/Data/Container/Indexed.agda @@ -11,7 +11,7 @@ module README.Data.Container.Indexed where open import Data.Unit open import Data.Empty open import Data.Nat.Base -open import Data.Product +open import Data.Product.Base using (_,_) open import Function open import Data.W.Indexed open import Data.Container.Indexed diff --git a/README/Data/Integer.agda b/README/Data/Integer.agda index e93333dcf5..23619757d3 100644 --- a/README/Data/Integer.agda +++ b/README/Data/Integer.agda @@ -51,7 +51,6 @@ ex₅ i j = ℤₚ.*-comm i j -- provides some combinators for equational reasoning. open P.≡-Reasoning -open import Data.Product ex₆ : ∀ i j → i * (j + + 0) ≡ j * i ex₆ i j = begin diff --git a/README/Data/List/Fresh.agda b/README/Data/List/Fresh.agda index 27f7eb7ca0..4723c0631e 100644 --- a/README/Data/List/Fresh.agda +++ b/README/Data/List/Fresh.agda @@ -12,7 +12,7 @@ open import Data.Nat open import Data.List.Base open import Data.List.Fresh open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs) -open import Data.Product +open import Data.Product.Base using (_,_; proj₁; proj₂) open import Relation.Nary using (⌊_⌋; fromWitness) -- A sorted list of natural numbers can be seen as a fresh list diff --git a/README/Data/Record.agda b/README/Data/Record.agda index 5800d11e54..da0ae70dc4 100644 --- a/README/Data/Record.agda +++ b/README/Data/Record.agda @@ -11,7 +11,7 @@ module README.Data.Record where -open import Data.Product +open import Data.Product.Base using (_,_) open import Data.String open import Function.Base using (flip) open import Level diff --git a/README/Data/Wrap.agda b/README/Data/Wrap.agda index 35009e4ed4..b92a8a3c81 100644 --- a/README/Data/Wrap.agda +++ b/README/Data/Wrap.agda @@ -13,7 +13,7 @@ open import Data.Wrap open import Algebra open import Data.Nat open import Data.Nat.Properties -open import Data.Product +open import Data.Product.Base using (_,_; ∃; ∃₂; _×_) open import Level using (Level) open import Relation.Binary diff --git a/README/Design/Decidability.agda b/README/Design/Decidability.agda index e615af282e..7d4bf8d62f 100644 --- a/README/Design/Decidability.agda +++ b/README/Design/Decidability.agda @@ -13,7 +13,7 @@ open import Data.List open import Data.List.Properties using (∷-injective) open import Data.Nat open import Data.Nat.Properties using (suc-injective) -open import Data.Product +open import Data.Product.Base using (uncurry) open import Data.Unit open import Function open import Relation.Binary.PropositionalEquality diff --git a/README/Foreign/Haskell.agda b/README/Foreign/Haskell.agda index 61e757ea8f..38c6c78c4e 100644 --- a/README/Foreign/Haskell.agda +++ b/README/Foreign/Haskell.agda @@ -22,7 +22,7 @@ open import Data.Bool.Base using (Bool; if_then_else_) open import Data.Char as Char open import Data.List.Base as List using (List; _∷_; []; takeWhile; dropWhile) open import Data.Maybe.Base using (Maybe; just; nothing) -open import Data.Product +open import Data.Product.Base using (_×_; _,_) open import Function open import Relation.Nullary.Decidable diff --git a/README/Inspect.agda b/README/Inspect.agda index cff492d008..f136f6fdba 100644 --- a/README/Inspect.agda +++ b/README/Inspect.agda @@ -14,7 +14,7 @@ module README.Inspect where open import Data.Nat.Base open import Data.Nat.Properties -open import Data.Product +open import Data.Product.Base using (_×_; _,_) open import Relation.Binary.PropositionalEquality ------------------------------------------------------------------------ diff --git a/README/Relation/Binary/TypeClasses.agda b/README/Relation/Binary/TypeClasses.agda index 023e98c3e4..a836389ee4 100644 --- a/README/Relation/Binary/TypeClasses.agda +++ b/README/Relation/Binary/TypeClasses.agda @@ -19,7 +19,7 @@ open import Data.List.Instances open import Data.List.Relation.Binary.Lex.NonStrict using (Lex-≤) open import Data.Nat.Base renaming (_≤_ to _≤ℕ_) open import Data.Nat.Instances -open import Data.Product +open import Data.Product.Base using (_×_; _,_; Σ) open import Data.Product.Instances open import Data.Unit.Base renaming (_≤_ to _≤⊤_) open import Data.Unit.Instances diff --git a/README/Text/Pretty.agda b/README/Text/Pretty.agda index 2525ff5242..855c599f08 100644 --- a/README/Text/Pretty.agda +++ b/README/Text/Pretty.agda @@ -14,7 +14,7 @@ open import Data.Bool.Base open import Data.List.Base as List open import Data.List.NonEmpty as List⁺ open import Data.Nat.Base -open import Data.Product +open import Data.Product.Base using (_×_; uncurry; _,_) open import Data.String.Base hiding (parens; _<+>_) open import Data.Vec.Base as Vec open import Function.Base diff --git a/src/Algebra/Construct/DirectProduct.agda b/src/Algebra/Construct/DirectProduct.agda index 7722662114..5f7b042017 100644 --- a/src/Algebra/Construct/DirectProduct.agda +++ b/src/Algebra/Construct/DirectProduct.agda @@ -16,7 +16,7 @@ module Algebra.Construct.DirectProduct where open import Algebra -open import Data.Product +open import Data.Product.Base using (_×_; zip; _,_; map; _<*>_; uncurry) open import Data.Product.Relation.Binary.Pointwise.NonDependent open import Level using (Level; _⊔_) diff --git a/src/Algebra/Construct/LexProduct.agda b/src/Algebra/Construct/LexProduct.agda index 1301ff7c04..984cdd57f2 100644 --- a/src/Algebra/Construct/LexProduct.agda +++ b/src/Algebra/Construct/LexProduct.agda @@ -8,7 +8,7 @@ open import Algebra open import Data.Bool using (true; false) -open import Data.Product +open import Data.Product.Base using (_×_; _,_) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (Pointwise) open import Data.Sum.Base using (inj₁; inj₂) open import Function.Base using (_∘_) diff --git a/src/Algebra/Lattice/Construct/DirectProduct.agda b/src/Algebra/Lattice/Construct/DirectProduct.agda index 9e2a825c99..0c68071a51 100644 --- a/src/Algebra/Lattice/Construct/DirectProduct.agda +++ b/src/Algebra/Lattice/Construct/DirectProduct.agda @@ -16,7 +16,7 @@ open import Algebra open import Algebra.Lattice import Algebra.Construct.DirectProduct as DirectProduct -open import Data.Product +open import Data.Product.Base using (_,_; _<*>_) open import Data.Product.Relation.Binary.Pointwise.NonDependent open import Level using (Level; _⊔_) diff --git a/src/Algebra/Module/Construct/DirectProduct.agda b/src/Algebra/Module/Construct/DirectProduct.agda index 3c168564bd..840cc42cab 100644 --- a/src/Algebra/Module/Construct/DirectProduct.agda +++ b/src/Algebra/Module/Construct/DirectProduct.agda @@ -14,7 +14,7 @@ module Algebra.Module.Construct.DirectProduct where open import Algebra.Bundles open import Algebra.Construct.DirectProduct open import Algebra.Module.Bundles -open import Data.Product +open import Data.Product.Base using (map; _,_; proj₁; proj₂) open import Data.Product.Relation.Binary.Pointwise.NonDependent open import Level diff --git a/src/Algebra/Module/Definitions/Left.agda b/src/Algebra/Module/Definitions/Left.agda index 1175292fcb..15c7f3534e 100644 --- a/src/Algebra/Module/Definitions/Left.agda +++ b/src/Algebra/Module/Definitions/Left.agda @@ -16,7 +16,6 @@ module Algebra.Module.Definitions.Left where open import Data.Sum -open import Data.Product ------------------------------------------------------------------------ -- Binary operations diff --git a/src/Algebra/Module/Definitions/Right.agda b/src/Algebra/Module/Definitions/Right.agda index 9f9dc67bf7..bbccdc23e0 100644 --- a/src/Algebra/Module/Definitions/Right.agda +++ b/src/Algebra/Module/Definitions/Right.agda @@ -15,7 +15,6 @@ module Algebra.Module.Definitions.Right {a b ℓb} (A : Set a) {B : Set b} (_≈_ : Rel B ℓb) where -open import Data.Product open import Data.Sum ------------------------------------------------------------------------ diff --git a/src/Algebra/Module/Morphism/ModuleHomomorphism.agda b/src/Algebra/Module/Morphism/ModuleHomomorphism.agda index 47ae46de10..704ec3863c 100644 --- a/src/Algebra/Module/Morphism/ModuleHomomorphism.agda +++ b/src/Algebra/Module/Morphism/ModuleHomomorphism.agda @@ -25,7 +25,7 @@ module Algebra.Module.Morphism.ModuleHomomorphism where open import Axiom.DoubleNegationElimination -open import Data.Product +open import Data.Product.Base using (∃₂; _×_; _,_) open import Relation.Binary.Reasoning.MultiSetoid open import Relation.Nullary using (¬_) open import Relation.Nullary.Negation using (contraposition) diff --git a/src/Algebra/Morphism/Construct/Composition.agda b/src/Algebra/Morphism/Construct/Composition.agda index 991fb93433..eb5a42e4bd 100644 --- a/src/Algebra/Morphism/Construct/Composition.agda +++ b/src/Algebra/Morphism/Construct/Composition.agda @@ -10,7 +10,6 @@ module Algebra.Morphism.Construct.Composition where open import Algebra.Bundles open import Algebra.Morphism.Structures -open import Data.Product open import Function.Base using (_∘_) import Function.Construct.Composition as Func open import Level using (Level) diff --git a/src/Algebra/Morphism/GroupMonomorphism.agda b/src/Algebra/Morphism/GroupMonomorphism.agda index b7a09ce92c..b862559938 100644 --- a/src/Algebra/Morphism/GroupMonomorphism.agda +++ b/src/Algebra/Morphism/GroupMonomorphism.agda @@ -26,7 +26,7 @@ open RawGroup G₂ renaming open import Algebra.Definitions open import Algebra.Structures -open import Data.Product +open import Data.Product.Base using (_,_) import Relation.Binary.Reasoning.Setoid as SetoidReasoning ------------------------------------------------------------------------ diff --git a/src/Algebra/Morphism/MagmaMonomorphism.agda b/src/Algebra/Morphism/MagmaMonomorphism.agda index c952fe112e..30f19edb02 100644 --- a/src/Algebra/Morphism/MagmaMonomorphism.agda +++ b/src/Algebra/Morphism/MagmaMonomorphism.agda @@ -25,7 +25,7 @@ open RawMagma M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_) open import Algebra.Structures open import Algebra.Definitions -open import Data.Product +open import Data.Product.Base using (map) open import Data.Sum.Base using (inj₁; inj₂) import Relation.Binary.Reasoning.Setoid as SetoidReasoning import Relation.Binary.Morphism.RelMonomorphism isRelMonomorphism as RelMorphism diff --git a/src/Algebra/Morphism/RingMonomorphism.agda b/src/Algebra/Morphism/RingMonomorphism.agda index f9789e60b7..4b2c900946 100644 --- a/src/Algebra/Morphism/RingMonomorphism.agda +++ b/src/Algebra/Morphism/RingMonomorphism.agda @@ -28,7 +28,7 @@ open RawRing R₂ renaming open import Algebra.Definitions open import Algebra.Structures -open import Data.Product +open import Data.Product.Base using (proj₁; proj₂; _,_) import Relation.Binary.Reasoning.Setoid as SetoidReasoning ------------------------------------------------------------------------ diff --git a/src/Algebra/Properties/Loop.agda b/src/Algebra/Properties/Loop.agda index 26bf6f4ce6..1ecb2c52f4 100644 --- a/src/Algebra/Properties/Loop.agda +++ b/src/Algebra/Properties/Loop.agda @@ -13,7 +13,6 @@ module Algebra.Properties.Loop {l₁ l₂} (L : Loop l₁ l₂) where open Loop L open import Algebra.Definitions _≈_ open import Relation.Binary.Reasoning.Setoid setoid -open import Data.Product open import Algebra.Properties.Quasigroup x//x≈ε : ∀ x → x // x ≈ ε diff --git a/src/Algebra/Properties/MiddleBolLoop.agda b/src/Algebra/Properties/MiddleBolLoop.agda index a50ce3b0d5..60f2898496 100644 --- a/src/Algebra/Properties/MiddleBolLoop.agda +++ b/src/Algebra/Properties/MiddleBolLoop.agda @@ -13,7 +13,6 @@ module Algebra.Properties.MiddleBolLoop {m₁ m₂} (M : MiddleBolLoop m₁ m₂ open MiddleBolLoop M open import Algebra.Definitions _≈_ open import Relation.Binary.Reasoning.Setoid setoid -open import Data.Product import Algebra.Properties.Loop as LoopProperties open LoopProperties loop public diff --git a/src/Algebra/Properties/MoufangLoop.agda b/src/Algebra/Properties/MoufangLoop.agda index 4740bc19b6..9b0e5ac94b 100644 --- a/src/Algebra/Properties/MoufangLoop.agda +++ b/src/Algebra/Properties/MoufangLoop.agda @@ -13,7 +13,7 @@ module Algebra.Properties.MoufangLoop {a ℓ} (M : MoufangLoop a ℓ) where open MoufangLoop M open import Algebra.Definitions _≈_ open import Relation.Binary.Reasoning.Setoid setoid -open import Data.Product +open import Data.Product.Base using (_,_) alternativeˡ : LeftAlternative _∙_ alternativeˡ x y = begin diff --git a/src/Algebra/Properties/Quasigroup.agda b/src/Algebra/Properties/Quasigroup.agda index a583ae34f5..335a9ea7a3 100644 --- a/src/Algebra/Properties/Quasigroup.agda +++ b/src/Algebra/Properties/Quasigroup.agda @@ -13,7 +13,7 @@ module Algebra.Properties.Quasigroup {q₁ q₂} (Q : Quasigroup q₁ q₂) wher open Quasigroup Q open import Algebra.Definitions _≈_ open import Relation.Binary.Reasoning.Setoid setoid -open import Data.Product +open import Data.Product.Base using (_,_) cancelˡ : LeftCancellative _∙_ cancelˡ x y z eq = begin diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda index 3006374347..c233a34b01 100644 --- a/src/Algebra/Solver/Monoid.agda +++ b/src/Algebra/Solver/Monoid.agda @@ -17,7 +17,7 @@ import Data.List.Relation.Binary.Equality.DecPropositional as ListEq open import Data.Maybe.Base as Maybe using (Maybe; decToMaybe; From-just; from-just) open import Data.Nat.Base using (ℕ) -open import Data.Product +open import Data.Product.Base using (_×_; uncurry) open import Data.Vec.Base using (Vec; lookup) open import Function.Base using (_∘_; _$_) open import Relation.Binary using (Decidable) diff --git a/src/Codata/Musical/Conversion.agda b/src/Codata/Musical/Conversion.agda index d7213daba9..4e5886e000 100644 --- a/src/Codata/Musical/Conversion.agda +++ b/src/Codata/Musical/Conversion.agda @@ -27,7 +27,7 @@ open import Codata.Musical.Covec hiding (module Covec) open import Codata.Musical.M hiding (module M) open import Codata.Musical.Notation open import Codata.Musical.Stream hiding (module Stream) -open import Data.Product +open import Data.Product.Base using (_,_) open import Data.Container.Core as C using (Container) import Size diff --git a/src/Codata/Musical/M/Indexed.agda b/src/Codata/Musical/M/Indexed.agda index 964aca0695..3eefda55e6 100644 --- a/src/Codata/Musical/M/Indexed.agda +++ b/src/Codata/Musical/M/Indexed.agda @@ -11,7 +11,7 @@ module Codata.Musical.M.Indexed where open import Level open import Codata.Musical.Notation -open import Data.Product +open import Data.Product.Base using (_,_; proj₁; proj₂) open import Data.Container.Indexed.Core open import Function.Base using (_∘_) open import Relation.Unary diff --git a/src/Data/AVL/IndexedMap.agda b/src/Data/AVL/IndexedMap.agda index 64a0d5c36a..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 as Prod +open import Data.Product.Base using (∃) open import Relation.Binary open import Relation.Binary.PropositionalEquality using (_≡_; cong; subst) import Data.Tree.AVL.Value diff --git a/src/Data/Container/Indexed/Core.agda b/src/Data/Container/Indexed/Core.agda index 91fb4b2e21..75d1a0d986 100644 --- a/src/Data/Container/Indexed/Core.agda +++ b/src/Data/Container/Indexed/Core.agda @@ -9,7 +9,7 @@ module Data.Container.Indexed.Core where open import Level -open import Data.Product +open import Data.Product.Base using (Σ; Σ-syntax; _,_; ∃) open import Relation.Unary infix 5 _◃_/_ diff --git a/src/Data/Container/Indexed/FreeMonad.agda b/src/Data/Container/Indexed/FreeMonad.agda index f2fe0d2aab..946e7540f3 100644 --- a/src/Data/Container/Indexed/FreeMonad.agda +++ b/src/Data/Container/Indexed/FreeMonad.agda @@ -15,7 +15,7 @@ open import Data.Container.Indexed open import Data.Container.Indexed.Combinator hiding (id; _∘_) open import Data.Empty open import Data.Sum.Base using (inj₁; inj₂) -open import Data.Product +open import Data.Product.Base using (_,_) open import Data.W.Indexed open import Relation.Unary open import Relation.Unary.PredicateTransformer diff --git a/src/Data/Integer/GCD.agda b/src/Data/Integer/GCD.agda index e087da4763..3f46877f45 100644 --- a/src/Data/Integer/GCD.agda +++ b/src/Data/Integer/GCD.agda @@ -13,7 +13,7 @@ open import Data.Integer.Divisibility open import Data.Integer.Properties open import Data.Nat.Base import Data.Nat.GCD as ℕ -open import Data.Product +open import Data.Product.Base using (_,_) open import Relation.Binary.PropositionalEquality open import Algebra.Definitions {A = ℤ} _≡_ as Algebra diff --git a/src/Data/List/Countdown.agda b/src/Data/List/Countdown.agda index fde7439ebf..50c87e8029 100644 --- a/src/Data/List/Countdown.agda +++ b/src/Data/List/Countdown.agda @@ -23,7 +23,7 @@ open import Data.Bool.Base using (true; false) open import Data.List.Base hiding (lookup) open import Data.List.Relation.Unary.Any as Any using (here; there) open import Data.Nat.Base using (ℕ; zero; suc) -open import Data.Product +open import Data.Product.Base using (∃; _,_; _×_) open import Data.Sum.Base open import Data.Sum.Properties open import Relation.Nullary.Reflects using (invert) diff --git a/src/Data/List/Relation/Binary/Lex/NonStrict.agda b/src/Data/List/Relation/Binary/Lex/NonStrict.agda index 83c8767cb3..3e42519be3 100644 --- a/src/Data/List/Relation/Binary/Lex/NonStrict.agda +++ b/src/Data/List/Relation/Binary/Lex/NonStrict.agda @@ -14,7 +14,6 @@ module Data.List.Relation.Binary.Lex.NonStrict where open import Data.Empty using (⊥) open import Function.Base open import Data.Unit.Base using (⊤; tt) -open import Data.Product open import Data.List.Base open import Data.List.Relation.Binary.Pointwise using (Pointwise; []) import Data.List.Relation.Binary.Lex.Strict as Strict diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda index 2fe2447efb..6bc602c7f2 100644 --- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda +++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda @@ -22,7 +22,7 @@ open import Level using (_⊔_) open import Data.Fin as Fin open import Data.Maybe.Base as M open import Data.Nat.Base as Nat using (ℕ) -open import Data.Product +open import Data.Product.Base using (Σ-syntax; _,_) open import Data.Vec.Base as Vec using (Vec ; lookup) open import Data.List.Base hiding (lookup) open import Data.List.Properties diff --git a/src/Data/Maybe/Relation/Binary/Connected.agda b/src/Data/Maybe/Relation/Binary/Connected.agda index e2fea581af..8f329b1440 100644 --- a/src/Data/Maybe/Relation/Binary/Connected.agda +++ b/src/Data/Maybe/Relation/Binary/Connected.agda @@ -9,7 +9,6 @@ module Data.Maybe.Relation.Binary.Connected where open import Level -open import Data.Product open import Data.Maybe.Base using (Maybe; just; nothing) open import Function.Bundles using (_⇔_; mk⇔) open import Relation.Binary hiding (_⇔_) diff --git a/src/Data/Maybe/Relation/Binary/Pointwise.agda b/src/Data/Maybe/Relation/Binary/Pointwise.agda index 389c1fde6e..85494cf29f 100644 --- a/src/Data/Maybe/Relation/Binary/Pointwise.agda +++ b/src/Data/Maybe/Relation/Binary/Pointwise.agda @@ -9,7 +9,7 @@ module Data.Maybe.Relation.Binary.Pointwise where open import Level -open import Data.Product +open import Data.Product.Base using (∃; _×_; -,_; _,_) open import Data.Maybe.Base using (Maybe; just; nothing) open import Function.Bundles using (_⇔_; mk⇔) open import Relation.Binary hiding (_⇔_) diff --git a/src/Data/Nat/GCD.agda b/src/Data/Nat/GCD.agda index fe90cc0282..a230e382ef 100644 --- a/src/Data/Nat/GCD.agda +++ b/src/Data/Nat/GCD.agda @@ -15,7 +15,8 @@ open import Data.Nat.GCD.Lemmas open import Data.Nat.Properties open import Data.Nat.Induction using (Acc; acc; <′-Rec; <′-recBuilder; <-wellFounded-fast) -open import Data.Product +open import Data.Product.Base + using (_×_; _,_; proj₂; proj₁; swap; uncurry′; ∃; map) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂) open import Function open import Induction using (build) diff --git a/src/Data/Nat/LCM.agda b/src/Data/Nat/LCM.agda index 9b8932785a..2d34586ee3 100644 --- a/src/Data/Nat/LCM.agda +++ b/src/Data/Nat/LCM.agda @@ -15,7 +15,7 @@ open import Data.Nat.Divisibility open import Data.Nat.DivMod open import Data.Nat.Properties open import Data.Nat.GCD -open import Data.Product +open import Data.Product.Base using (_×_; _,_; uncurry′; ∃) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Function open import Relation.Binary.PropositionalEquality as P diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index e634095eea..e3c1986ff2 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -13,7 +13,7 @@ open import Data.Nat.Base open import Data.Nat.Divisibility open import Data.Nat.GCD using (module GCD; module Bézout) open import Data.Nat.Properties -open import Data.Product +open import Data.Product.Base using (∃; _×_; map₂; _,_) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Function.Base using (flip; _∘_; _∘′_) open import Relation.Nullary.Decidable as Dec diff --git a/src/Data/Product/Effectful/Examples.agda b/src/Data/Product/Effectful/Examples.agda index 90488642f6..e81890172c 100644 --- a/src/Data/Product/Effectful/Examples.agda +++ b/src/Data/Product/Effectful/Examples.agda @@ -14,7 +14,7 @@ module Data.Product.Effectful.Examples open import Level using (Lift; lift; _⊔_) open import Effect.Functor using (RawFunctor) open import Effect.Monad using (RawMonad) -open import Data.Product +open import Data.Product.Base using (_×_; _,_) open import Data.Product.Relation.Binary.Pointwise.NonDependent open import Function import Function.Identity.Effectful as Id diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda index d062e33d39..abae430992 100644 --- a/src/Data/Product/Function/Dependent/Propositional.agda +++ b/src/Data/Product/Function/Dependent/Propositional.agda @@ -9,7 +9,7 @@ module Data.Product.Function.Dependent.Propositional where -open import Data.Product +open import Data.Product.Base using (Σ; map; _,_) open import Data.Product.Function.NonDependent.Setoid open import Data.Product.Relation.Binary.Pointwise.NonDependent open import Relation.Binary hiding (_⇔_) diff --git a/src/Data/Product/Function/Dependent/Propositional/WithK.agda b/src/Data/Product/Function/Dependent/Propositional/WithK.agda index 0b3838e12f..df3bafe613 100644 --- a/src/Data/Product/Function/Dependent/Propositional/WithK.agda +++ b/src/Data/Product/Function/Dependent/Propositional/WithK.agda @@ -9,7 +9,7 @@ module Data.Product.Function.Dependent.Propositional.WithK where -open import Data.Product +open import Data.Product.Base using (Σ) open import Data.Product.Function.Dependent.Setoid open import Data.Product.Relation.Binary.Pointwise.Dependent open import Data.Product.Relation.Binary.Pointwise.Dependent.WithK diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda index f6629e048a..9e6ef09a67 100644 --- a/src/Data/Product/Function/Dependent/Setoid.agda +++ b/src/Data/Product/Function/Dependent/Setoid.agda @@ -9,7 +9,7 @@ module Data.Product.Function.Dependent.Setoid where -open import Data.Product +open import Data.Product.Base using (map; _,_) open import Data.Product.Relation.Binary.Pointwise.Dependent open import Function.Base open import Function.Equality as F using (_⟶_; _⟨$⟩_) diff --git a/src/Data/Product/Function/Dependent/Setoid/WithK.agda b/src/Data/Product/Function/Dependent/Setoid/WithK.agda index a343e22b43..602bd31507 100644 --- a/src/Data/Product/Function/Dependent/Setoid/WithK.agda +++ b/src/Data/Product/Function/Dependent/Setoid/WithK.agda @@ -9,7 +9,7 @@ module Data.Product.Function.Dependent.Setoid.WithK where -open import Data.Product +open import Data.Product.Base using (_,_) open import Data.Product.Function.Dependent.Setoid using (surjection) open import Data.Product.Relation.Binary.Pointwise.Dependent open import Relation.Binary diff --git a/src/Data/Product/Function/NonDependent/Propositional.agda b/src/Data/Product/Function/NonDependent/Propositional.agda index e686cbad6e..b4c9501304 100644 --- a/src/Data/Product/Function/NonDependent/Propositional.agda +++ b/src/Data/Product/Function/NonDependent/Propositional.agda @@ -9,7 +9,7 @@ module Data.Product.Function.NonDependent.Propositional where -open import Data.Product +open import Data.Product.Base using (_×_; map) open import Data.Product.Function.NonDependent.Setoid open import Data.Product.Relation.Binary.Pointwise.NonDependent open import Relation.Binary hiding (_⇔_) diff --git a/src/Data/Product/Function/NonDependent/Setoid.agda b/src/Data/Product/Function/NonDependent/Setoid.agda index eb1a369710..93e388da23 100644 --- a/src/Data/Product/Function/NonDependent/Setoid.agda +++ b/src/Data/Product/Function/NonDependent/Setoid.agda @@ -9,7 +9,7 @@ module Data.Product.Function.NonDependent.Setoid where -open import Data.Product +open import Data.Product.Base using (map; _,_; <_,_>; proj₁; proj₂) open import Data.Product.Relation.Binary.Pointwise.NonDependent open import Relation.Binary open import Function.Equality as F using (_⟶_; _⟨$⟩_) diff --git a/src/Data/Product/Properties/WithK.agda b/src/Data/Product/Properties/WithK.agda index 2218ec4ca3..e68e51f52e 100644 --- a/src/Data/Product/Properties/WithK.agda +++ b/src/Data/Product/Properties/WithK.agda @@ -8,7 +8,7 @@ module Data.Product.Properties.WithK where -open import Data.Product +open import Data.Product.Base using (Σ; _,_) open import Function open import Relation.Binary.PropositionalEquality diff --git a/src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda b/src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda index c1228b5a91..6fc53e658c 100644 --- a/src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda +++ b/src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda @@ -9,7 +9,7 @@ module Data.Product.Relation.Binary.Pointwise.Dependent.WithK where -open import Data.Product +open import Data.Product.Base using (Σ; uncurry) open import Data.Product.Relation.Binary.Pointwise.Dependent open import Function.Base open import Function.Inverse using (Inverse) diff --git a/src/Data/Sum/Relation/Binary/LeftOrder.agda b/src/Data/Sum/Relation/Binary/LeftOrder.agda index 063ba49bb7..4036285a41 100644 --- a/src/Data/Sum/Relation/Binary/LeftOrder.agda +++ b/src/Data/Sum/Relation/Binary/LeftOrder.agda @@ -11,7 +11,7 @@ module Data.Sum.Relation.Binary.LeftOrder where open import Data.Sum.Base as Sum open import Data.Sum.Relation.Binary.Pointwise as PW using (Pointwise; inj₁; inj₂) -open import Data.Product +open import Data.Product.Base using (_,_) open import Data.Empty open import Function open import Level diff --git a/src/Data/These/Properties.agda b/src/Data/These/Properties.agda index 62257ed1ad..5e77dd483a 100644 --- a/src/Data/These/Properties.agda +++ b/src/Data/These/Properties.agda @@ -8,7 +8,7 @@ module Data.These.Properties where -open import Data.Product +open import Data.Product.Base using (_×_; _,_; <_,_>; uncurry) open import Data.These.Base open import Function.Base using (_∘_) open import Relation.Binary using (Decidable) diff --git a/src/Data/Tree/AVL/Indexed/WithK.agda b/src/Data/Tree/AVL/Indexed/WithK.agda index 2ef4ec3544..e19b231b0b 100644 --- a/src/Data/Tree/AVL/Indexed/WithK.agda +++ b/src/Data/Tree/AVL/Indexed/WithK.agda @@ -15,7 +15,6 @@ module Data.Tree.AVL.Indexed.WithK strictTotalOrder = record { isStrictTotalOrder = isStrictTotalOrder } -open import Data.Product open import Data.Tree.AVL.Indexed strictTotalOrder as AVL hiding (Value) module _ {v} {V′ : Key → Set v} where diff --git a/src/Data/Tree/AVL/Key.agda b/src/Data/Tree/AVL/Key.agda index dc7e77824d..110c2b9ab7 100644 --- a/src/Data/Tree/AVL/Key.agda +++ b/src/Data/Tree/AVL/Key.agda @@ -16,7 +16,7 @@ module Data.Tree.AVL.Key open import Level open import Data.Empty open import Data.Unit -open import Data.Product +open import Data.Product.Base using (_×_; _,_) open import Relation.Binary.PropositionalEquality using (_≡_ ; refl) open import Relation.Nullary.Negation using (¬_) open import Relation.Nullary.Construct.Add.Extrema diff --git a/src/Data/Universe.agda b/src/Data/Universe.agda index 516e0bd2a4..9bbfb4620b 100644 --- a/src/Data/Universe.agda +++ b/src/Data/Universe.agda @@ -8,7 +8,6 @@ module Data.Universe where -open import Data.Product open import Level ------------------------------------------------------------------------ diff --git a/src/Data/Universe/Indexed.agda b/src/Data/Universe/Indexed.agda index a11958e16f..26b77a1fb0 100644 --- a/src/Data/Universe/Indexed.agda +++ b/src/Data/Universe/Indexed.agda @@ -8,7 +8,7 @@ module Data.Universe.Indexed where -open import Data.Product +open import Data.Product.Base using (∃; proj₂) open import Data.Universe open import Function open import Level diff --git a/src/Data/W/Indexed.agda b/src/Data/W/Indexed.agda index b356a22533..fbf3910427 100644 --- a/src/Data/W/Indexed.agda +++ b/src/Data/W/Indexed.agda @@ -10,7 +10,7 @@ module Data.W.Indexed where open import Level open import Data.Container.Indexed.Core -open import Data.Product +open import Data.Product.Base using (_,_; Σ) open import Relation.Unary -- The family of indexed W-types. diff --git a/src/Data/W/WithK.agda b/src/Data/W/WithK.agda index 0646bfb315..e88fb7cda5 100644 --- a/src/Data/W/WithK.agda +++ b/src/Data/W/WithK.agda @@ -8,7 +8,7 @@ module Data.W.WithK where -open import Data.Product +open import Data.Product.Base using (_,_) open import Data.Container.Core open import Data.W open import Agda.Builtin.Equality diff --git a/src/Effect/Applicative/Predicate.agda b/src/Effect/Applicative/Predicate.agda index 0bfe6a9803..84e5b8a50a 100644 --- a/src/Effect/Applicative/Predicate.agda +++ b/src/Effect/Applicative/Predicate.agda @@ -12,7 +12,7 @@ module Effect.Applicative.Predicate where open import Effect.Functor.Predicate -open import Data.Product +open import Data.Product.Base using (_,_) open import Function open import Level open import Relation.Unary diff --git a/src/Effect/Monad/Predicate.agda b/src/Effect/Monad/Predicate.agda index 5593b202d8..510556ee9c 100644 --- a/src/Effect/Monad/Predicate.agda +++ b/src/Effect/Monad/Predicate.agda @@ -14,7 +14,7 @@ open import Effect.Applicative.Indexed open import Effect.Monad open import Effect.Monad.Indexed open import Data.Unit -open import Data.Product +open import Data.Product.Base using (_,_) open import Function open import Level open import Relation.Binary.PropositionalEquality diff --git a/src/Effect/Monad/State.agda b/src/Effect/Monad/State.agda index 222f6e7f48..41fc3336d8 100644 --- a/src/Effect/Monad/State.agda +++ b/src/Effect/Monad/State.agda @@ -9,7 +9,7 @@ module Effect.Monad.State where -open import Data.Product +open import Data.Product.Base using (_×_) open import Effect.Choice open import Effect.Empty open import Effect.Functor diff --git a/src/Effect/Monad/State/Indexed.agda b/src/Effect/Monad/State/Indexed.agda index 1fc27655d8..4150554ac9 100644 --- a/src/Effect/Monad/State/Indexed.agda +++ b/src/Effect/Monad/State/Indexed.agda @@ -12,7 +12,7 @@ open import Effect.Applicative.Indexed open import Effect.Monad open import Function.Identity.Effectful as Id using (Identity) open import Effect.Monad.Indexed -open import Data.Product +open import Data.Product.Base using (_×_; _,_; uncurry) open import Data.Unit open import Function.Base open import Level diff --git a/src/Function/Bijection.agda b/src/Function/Bijection.agda index 1de607e957..8c7ce78ef3 100644 --- a/src/Function/Bijection.agda +++ b/src/Function/Bijection.agda @@ -13,7 +13,6 @@ module Function.Bijection where -open import Data.Product open import Level open import Relation.Binary open import Relation.Binary.PropositionalEquality as P diff --git a/src/Function/Endomorphism/Setoid.agda b/src/Function/Endomorphism/Setoid.agda index b02976db88..9d7974294c 100644 --- a/src/Function/Endomorphism/Setoid.agda +++ b/src/Function/Endomorphism/Setoid.agda @@ -21,7 +21,7 @@ open import Algebra.Morphism; open Definitions open import Function.Equality open import Data.Nat.Base using (ℕ; _+_); open ℕ open import Data.Nat.Properties -open import Data.Product +open import Data.Product.Base using (_,_) import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial as Trivial diff --git a/src/Function/LeftInverse.agda b/src/Function/LeftInverse.agda index f06fbc6c8a..23f9b4a900 100644 --- a/src/Function/LeftInverse.agda +++ b/src/Function/LeftInverse.agda @@ -13,7 +13,6 @@ module Function.LeftInverse where -open import Data.Product open import Level import Relation.Binary.Reasoning.Setoid as EqReasoning open import Relation.Binary diff --git a/src/Function/Properties/RightInverse.agda b/src/Function/Properties/RightInverse.agda index f5aa05d9df..2d82937ddb 100644 --- a/src/Function/Properties/RightInverse.agda +++ b/src/Function/Properties/RightInverse.agda @@ -12,7 +12,7 @@ open import Function.Base open import Function.Bundles open import Function.Consequences using (inverseʳ⇒surjective) open import Level using (Level) -open import Data.Product +open import Data.Product.Base using (_,_) open import Relation.Binary using (Setoid; IsEquivalence) private diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda index ab164c43d0..977165a046 100644 --- a/src/Function/Properties/Surjection.agda +++ b/src/Function/Properties/Surjection.agda @@ -11,7 +11,7 @@ module Function.Properties.Surjection where open import Function.Base open import Function.Bundles open import Level using (Level) -open import Data.Product +open import Data.Product.Base using (proj₁; proj₂) private variable diff --git a/src/Function/Surjection.agda b/src/Function/Surjection.agda index 12f4490f3e..6861979551 100644 --- a/src/Function/Surjection.agda +++ b/src/Function/Surjection.agda @@ -19,7 +19,6 @@ open import Function.Equality as F open import Function.Equivalence using (Equivalence) open import Function.Injection hiding (id; _∘_; injection) open import Function.LeftInverse as Left hiding (id; _∘_) -open import Data.Product open import Relation.Binary open import Relation.Binary.PropositionalEquality as P using (_≡_) diff --git a/src/Induction/Lexicographic.agda b/src/Induction/Lexicographic.agda index 303f2c8dfa..6acd96b7f1 100644 --- a/src/Induction/Lexicographic.agda +++ b/src/Induction/Lexicographic.agda @@ -8,7 +8,7 @@ module Induction.Lexicographic where -open import Data.Product +open import Data.Product.Base using (Σ; _,_; _×_) open import Induction open import Level diff --git a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda index 45463af482..785213c792 100644 --- a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda +++ b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda @@ -15,7 +15,7 @@ module Relation.Binary.Construct.Add.Infimum.Strict {a ℓ} {A : Set a} (_<_ : Rel A ℓ) where open import Level using (_⊔_) -open import Data.Product +open import Data.Product.Base using (_,_; map) open import Function.Base open import Relation.Binary.PropositionalEquality as P using (_≡_; refl) diff --git a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda index 46415e6895..10588a0d6a 100644 --- a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda +++ b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda @@ -15,7 +15,7 @@ module Relation.Binary.Construct.Add.Supremum.Strict {a r} {A : Set a} (_<_ : Rel A r) where open import Level using (_⊔_) -open import Data.Product +open import Data.Product.Base using (_,_; map) open import Function.Base open import Relation.Nullary hiding (Irrelevant) import Relation.Nullary.Decidable as Dec diff --git a/src/Relation/Binary/Construct/Composition.agda b/src/Relation/Binary/Construct/Composition.agda index e34550fb58..7f8ba241b0 100644 --- a/src/Relation/Binary/Construct/Composition.agda +++ b/src/Relation/Binary/Construct/Composition.agda @@ -8,7 +8,7 @@ module Relation.Binary.Construct.Composition where -open import Data.Product +open import Data.Product.Base using (∃; _×_; _,_) open import Function.Base open import Level open import Relation.Binary diff --git a/src/Relation/Binary/Construct/Flip/Ord.agda b/src/Relation/Binary/Construct/Flip/Ord.agda index ecfc4b6df4..4a2eea690f 100644 --- a/src/Relation/Binary/Construct/Flip/Ord.agda +++ b/src/Relation/Binary/Construct/Flip/Ord.agda @@ -12,7 +12,7 @@ open import Relation.Binary module Relation.Binary.Construct.Flip.Ord where -open import Data.Product +open import Data.Product.Base using (_,_) open import Function.Base using (flip; _∘_) open import Level using (Level) diff --git a/src/Relation/Binary/Construct/FromPred.agda b/src/Relation/Binary/Construct/FromPred.agda index c95f95fb6f..e08997b9a7 100644 --- a/src/Relation/Binary/Construct/FromPred.agda +++ b/src/Relation/Binary/Construct/FromPred.agda @@ -16,7 +16,6 @@ module Relation.Binary.Construct.FromPred where open import Function.Base -open import Data.Product open module Eq = Setoid S using (_≈_) renaming (Carrier to A) diff --git a/src/Relation/Binary/Construct/FromRel.agda b/src/Relation/Binary/Construct/FromRel.agda index fb842b7810..13fc1774c7 100644 --- a/src/Relation/Binary/Construct/FromRel.agda +++ b/src/Relation/Binary/Construct/FromRel.agda @@ -15,7 +15,6 @@ module Relation.Binary.Construct.FromRel {a r} {A : Set a} (_R_ : REL A (Carrier S) r) -- The relation where -open import Data.Product open import Function.Base open import Level using (_⊔_) diff --git a/src/Relation/Binary/Construct/On.agda b/src/Relation/Binary/Construct/On.agda index 5206276f95..122b0d6584 100644 --- a/src/Relation/Binary/Construct/On.agda +++ b/src/Relation/Binary/Construct/On.agda @@ -8,7 +8,7 @@ module Relation.Binary.Construct.On where -open import Data.Product +open import Data.Product.Base using (_,_) open import Function.Base using (_on_; _∘_) open import Induction.WellFounded using (WellFounded; Acc; acc) open import Level using (Level) diff --git a/src/Relation/Binary/HeterogeneousEquality.agda b/src/Relation/Binary/HeterogeneousEquality.agda index 0a4886531e..87b8916d25 100644 --- a/src/Relation/Binary/HeterogeneousEquality.agda +++ b/src/Relation/Binary/HeterogeneousEquality.agda @@ -9,7 +9,6 @@ module Relation.Binary.HeterogeneousEquality where import Axiom.Extensionality.Heterogeneous as Ext -open import Data.Product open import Data.Unit.NonEta open import Function.Base open import Function.Inverse using (Inverse) diff --git a/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda b/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda index fb1db6b9fb..e97cc02c67 100644 --- a/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda +++ b/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda @@ -15,7 +15,7 @@ open import Relation.Binary.HeterogeneousEquality hiding (isEquivalence) import Relation.Binary.PropositionalEquality as ≡ open import Data.Nat.Base open import Data.Nat.Properties -open import Data.Product +open import Data.Product.Base using (_×_; _,_) open import Function.Base open ≅-Reasoning diff --git a/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda b/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda index b75cfa7093..a86918081f 100644 --- a/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda +++ b/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda @@ -16,7 +16,7 @@ open BoundedJoinSemilattice J open import Algebra.Definitions _≈_ open import Algebra.Ordered.Structures using (IsCommutativePomonoid) open import Algebra.Ordered.Bundles using (CommutativePomonoid) -open import Data.Product +open import Data.Product.Base using (_,_) open import Function.Base using (_∘_; flip) open import Relation.Binary open import Relation.Binary.Properties.Poset poset diff --git a/src/Relation/Binary/Lattice/Properties/BoundedMeetSemilattice.agda b/src/Relation/Binary/Lattice/Properties/BoundedMeetSemilattice.agda index b6c7be5a5c..622c8b6b0c 100644 --- a/src/Relation/Binary/Lattice/Properties/BoundedMeetSemilattice.agda +++ b/src/Relation/Binary/Lattice/Properties/BoundedMeetSemilattice.agda @@ -14,7 +14,6 @@ module Relation.Binary.Lattice.Properties.BoundedMeetSemilattice open BoundedMeetSemilattice M open import Algebra.Definitions _≈_ -open import Data.Product open import Function.Base using (_∘_; flip) open import Relation.Binary open import Relation.Binary.Properties.Poset poset diff --git a/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda b/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda index fb85a17fe0..faa51120cd 100644 --- a/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda +++ b/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda @@ -18,7 +18,7 @@ import Algebra.Structures as Alg open import Algebra.Definitions _≈_ open import Algebra.Ordered.Structures using (IsPosemigroup) open import Algebra.Ordered.Bundles using (Posemigroup) -open import Data.Product +open import Data.Product.Base using (_,_) open import Function.Base using (_∘_; flip) open import Relation.Binary open import Relation.Binary.Properties.Poset poset diff --git a/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda b/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda index 34e4252f92..f072cb2199 100644 --- a/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda +++ b/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda @@ -14,7 +14,6 @@ module Relation.Binary.Lattice.Properties.MeetSemilattice open MeetSemilattice M open import Algebra.Definitions _≈_ -open import Data.Product open import Function.Base using (flip) open import Relation.Binary open import Relation.Binary.Properties.Poset poset diff --git a/src/Relation/Unary/PredicateTransformer.agda b/src/Relation/Unary/PredicateTransformer.agda index 518552d0d8..05d33d3b94 100644 --- a/src/Relation/Unary/PredicateTransformer.agda +++ b/src/Relation/Unary/PredicateTransformer.agda @@ -8,7 +8,7 @@ module Relation.Unary.PredicateTransformer where -open import Data.Product +open import Data.Product.Base using (∃) open import Function open import Level hiding (_⊔_) open import Relation.Nullary diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda index 25e21193be..236831d281 100644 --- a/src/Tactic/Cong.agda +++ b/src/Tactic/Cong.agda @@ -34,7 +34,7 @@ open import Data.Maybe.Base as Maybe using (Maybe; just; nothing) open import Data.Nat.Base as Nat using (ℕ; zero; suc; _≡ᵇ_; _+_) open import Data.Unit.Base using (⊤) open import Data.Word.Base as Word using (toℕ) -open import Data.Product +open import Data.Product.Base using (_×_; map₁; _,_) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong) diff --git a/src/Tactic/RingSolver/NonReflective.agda b/src/Tactic/RingSolver/NonReflective.agda index 1c65a6c1bb..3a13e1d1e7 100644 --- a/src/Tactic/RingSolver/NonReflective.agda +++ b/src/Tactic/RingSolver/NonReflective.agda @@ -23,7 +23,7 @@ open import Data.Bool.Base using (Bool; true; false; T; if_then_else_) open import Data.Maybe.Base open import Data.Empty using (⊥-elim) open import Data.Nat.Base using (ℕ) -open import Data.Product +open import Data.Product.Base using (_×_; proj₁; proj₂; _,_) open import Data.Vec hiding (_⊛_) open import Data.Vec.N-ary diff --git a/src/Text/Format/Generic.agda b/src/Text/Format/Generic.agda index d0fe551041..dc78db2c3f 100644 --- a/src/Text/Format/Generic.agda +++ b/src/Text/Format/Generic.agda @@ -14,7 +14,7 @@ open import Data.Char.Base using (Char) open import Data.List.Base as List open import Data.Maybe.Base as Maybe open import Data.Nat.Base -open import Data.Product +open import Data.Product.Base using (_,_) open import Data.Product.Nary.NonDependent open import Data.Sum.Base open import Data.String.Base From b31ab2b369b18229db07f762296d1177aacbab46 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Thu, 29 Jun 2023 12:50:17 -0400 Subject: [PATCH 2/5] Final `Data.Product` imports simplified --- README/Data/Trie/NonDependent.agda | 4 ++-- src/Algebra/Apartness/Structures.agda | 2 +- src/Algebra/Properties/Magma/Divisibility.agda | 2 +- src/Codata/Musical/Colist.agda | 2 +- src/Codata/Musical/Colist/Infinite-merge.agda | 2 +- src/Data/Container/Combinator.agda | 2 +- src/Data/Container/Combinator/Properties.agda | 2 +- src/Data/Container/Indexed/Combinator.agda | 2 +- src/Data/Container/Indexed/WithK.agda | 3 ++- src/Data/Container/Morphism/Properties.agda | 2 +- src/Data/Container/Relation/Unary/All.agda | 2 +- src/Data/Container/Relation/Unary/Any.agda | 2 +- src/Data/Container/Relation/Unary/Any/Properties.agda | 2 +- src/Data/Fin/Subset.agda | 2 +- src/Data/Graph/Acyclic.agda | 2 +- src/Data/List/Fresh/Membership/Setoid/Properties.agda | 2 +- src/Data/List/Fresh/Relation/Unary/Any.agda | 2 +- src/Data/List/Membership/Propositional/Properties.agda | 2 +- .../List/Membership/Propositional/Properties/Core.agda | 2 +- src/Data/List/Membership/Setoid/Properties.agda | 2 +- src/Data/List/Relation/Binary/BagAndSetEquality.agda | 2 +- .../Binary/Permutation/Propositional/Properties.agda | 2 +- .../Relation/Binary/Permutation/Setoid/Properties.agda | 2 +- src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda | 2 +- .../Relation/Binary/Sublist/Heterogeneous/Properties.agda | 2 +- .../Relation/Binary/Sublist/Propositional/Properties.agda | 2 +- src/Data/List/Relation/Binary/Sublist/Setoid.agda | 2 +- .../List/Relation/Binary/Sublist/Setoid/Properties.agda | 2 +- src/Data/List/Relation/Ternary/Appending.agda | 2 +- src/Data/List/Relation/Ternary/Interleaving.agda | 2 +- src/Data/List/Relation/Unary/Any/Properties.agda | 2 +- src/Data/List/Relation/Unary/First.agda | 2 +- src/Data/Maybe/Relation/Unary/Any.agda | 2 +- src/Data/Nat/Binary/Properties.agda | 2 +- src/Data/Nat/Binary/Subtraction.agda | 2 +- src/Data/Nat/InfinitelyOften.agda | 2 +- src/Data/Tree/AVL/Indexed.agda | 2 +- src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda | 2 +- .../Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda | 2 +- src/Data/Tree/AVL/IndexedMap.agda | 7 ++++--- src/Data/Tree/AVL/Map/Membership/Propositional.agda | 2 +- .../Tree/AVL/Map/Membership/Propositional/Properties.agda | 2 +- src/Data/Tree/AVL/Map/Relation/Unary/Any.agda | 2 +- src/Data/Tree/AVL/Relation/Unary/Any.agda | 2 +- src/Data/Trie.agda | 2 +- src/Data/Trie/NonEmpty.agda | 2 +- src/Data/Vec/Functional/Relation/Unary/Any.agda | 2 +- src/Data/Vec/Membership/Propositional/Properties.agda | 4 ++-- src/Data/Vec/Membership/Setoid.agda | 2 +- src/Data/Vec/Relation/Unary/Any.agda | 2 +- src/Data/Vec/Relation/Unary/Any/Properties.agda | 2 +- src/Function/Related/TypeIsomorphisms.agda | 3 ++- src/Relation/Binary/Rewriting.agda | 2 +- src/Relation/Unary/Indexed.agda | 2 +- tests/data/trie/Main.agda | 4 ++-- 55 files changed, 63 insertions(+), 60 deletions(-) diff --git a/README/Data/Trie/NonDependent.agda b/README/Data/Trie/NonDependent.agda index 9921942f6d..33e2126988 100644 --- a/README/Data/Trie/NonDependent.agda +++ b/README/Data/Trie/NonDependent.agda @@ -56,7 +56,7 @@ import Data.Char.Properties as Char open import Data.List.Base as List using (List; []; _∷_) open import Data.List.Fresh as List# using (List#; []; _∷#_) open import Data.Maybe as Maybe -open import Data.Product as Prod +open import Data.Product.Base using (map₁; _×_; ∃; proj₁; _,_) open import Data.String.Base as String using (String) open import Data.String.Properties as String using (_≟_) open import Data.These as These @@ -127,7 +127,7 @@ module _ {t} (L : Lexer t) where -- characters one by one init : Keywords - init = fromList $ List.map (Prod.map₁ String.toList) $ proj₁ $ List#.toList keywords + init = fromList $ List.map (map₁ String.toList) $ proj₁ $ List#.toList keywords -- Kickstart the tokeniser with an empty accumulator and the initial -- trie. diff --git a/src/Algebra/Apartness/Structures.agda b/src/Algebra/Apartness/Structures.agda index 3311234945..a8c5c88982 100644 --- a/src/Algebra/Apartness/Structures.agda +++ b/src/Algebra/Apartness/Structures.agda @@ -17,7 +17,7 @@ module Algebra.Apartness.Structures where open import Level using (_⊔_; suc) -open import Data.Product using (∃-syntax; _×_; _,_; proj₂) +open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₂) open import Algebra.Definitions _≈_ using (Invertible) open import Algebra.Structures _≈_ using (IsCommutativeRing) open import Relation.Binary.Structures using (IsEquivalence; IsApartnessRelation) diff --git a/src/Algebra/Properties/Magma/Divisibility.agda b/src/Algebra/Properties/Magma/Divisibility.agda index 72907929df..d8ffc208f0 100644 --- a/src/Algebra/Properties/Magma/Divisibility.agda +++ b/src/Algebra/Properties/Magma/Divisibility.agda @@ -7,7 +7,7 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra using (Magma) -open import Data.Product using (_×_; _,_; ∃; map; swap) +open import Data.Product.Base using (_×_; _,_; ∃; map; swap) open import Relation.Binary.Definitions module Algebra.Properties.Magma.Divisibility {a ℓ} (M : Magma a ℓ) where diff --git a/src/Codata/Musical/Colist.agda b/src/Codata/Musical/Colist.agda index d70a101f6a..3ef672abc7 100644 --- a/src/Codata/Musical/Colist.agda +++ b/src/Codata/Musical/Colist.agda @@ -21,7 +21,7 @@ open import Data.Maybe.Relation.Unary.Any using (just) open import Data.Nat.Base using (ℕ; zero; suc) open import Data.List.Base using (List; []; _∷_) open import Data.List.NonEmpty using (List⁺; _∷_) -open import Data.Product as Prod using (∃; _×_; _,_) +open import Data.Product.Base as Prod using (∃; _×_; _,_) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′) open import Data.Vec.Bounded as Vec≤ using (Vec≤) open import Function.Base diff --git a/src/Codata/Musical/Colist/Infinite-merge.agda b/src/Codata/Musical/Colist/Infinite-merge.agda index 677024808a..eb06c3b9cc 100644 --- a/src/Codata/Musical/Colist/Infinite-merge.agda +++ b/src/Codata/Musical/Colist/Infinite-merge.agda @@ -13,7 +13,7 @@ open import Codata.Musical.Colist as Colist hiding (_⋎_) open import Data.Nat.Base open import Data.Nat.Induction using (<′-wellFounded) open import Data.Nat.Properties -open import Data.Product as Prod +open import Data.Product.Base as Prod using (_×_; _,_; ∃; ∃₂; proj₁; proj₂) open import Data.Sum.Base open import Data.Sum.Properties open import Data.Sum.Function.Propositional using (_⊎-cong_) diff --git a/src/Data/Container/Combinator.agda b/src/Data/Container/Combinator.agda index c68536427b..01e102cd5c 100644 --- a/src/Data/Container/Combinator.agda +++ b/src/Data/Container/Combinator.agda @@ -10,7 +10,7 @@ module Data.Container.Combinator where open import Level using (Level; _⊔_; lower) open import Data.Empty.Polymorphic using (⊥; ⊥-elim) -open import Data.Product as P using (_,_; <_,_>; proj₁; proj₂; ∃) +open import Data.Product.Base as P using (_,_; <_,_>; proj₁; proj₂; ∃) open import Data.Sum.Base as S using ([_,_]′) open import Data.Unit.Polymorphic.Base using (⊤) import Function.Base as F diff --git a/src/Data/Container/Combinator/Properties.agda b/src/Data/Container/Combinator/Properties.agda index b93d6c7a7a..8d347abcae 100644 --- a/src/Data/Container/Combinator/Properties.agda +++ b/src/Data/Container/Combinator/Properties.agda @@ -13,7 +13,7 @@ open import Data.Container.Core open import Data.Container.Combinator open import Data.Container.Relation.Unary.Any open import Data.Empty using (⊥-elim) -open import Data.Product as Prod using (∃; _,_; proj₁; proj₂; <_,_>; uncurry; curry) +open import Data.Product.Base as Prod using (∃; _,_; proj₁; proj₂; <_,_>; uncurry; curry) open import Data.Sum.Base as S using (inj₁; inj₂; [_,_]′; [_,_]) open import Function.Base as F using (_∘′_) open import Function.Inverse as Inv using (_↔_; inverse; module Inverse) diff --git a/src/Data/Container/Indexed/Combinator.agda b/src/Data/Container/Indexed/Combinator.agda index 43721d4689..283a6a0314 100644 --- a/src/Data/Container/Indexed/Combinator.agda +++ b/src/Data/Container/Indexed/Combinator.agda @@ -12,7 +12,7 @@ open import Axiom.Extensionality.Propositional using (Extensionality) open import Data.Container.Indexed open import Data.Empty.Polymorphic using (⊥; ⊥-elim) open import Data.Unit.Polymorphic.Base using (⊤) -open import Data.Product as Prod hiding (Σ) renaming (_×_ to _⟨×⟩_) +open import Data.Product.Base as Prod hiding (Σ) renaming (_×_ to _⟨×⟩_) open import Data.Sum.Base renaming (_⊎_ to _⟨⊎⟩_) open import Data.Sum.Relation.Unary.All as All using (All) open import Function.Base as F hiding (id; const) renaming (_∘_ to _⟨∘⟩_) diff --git a/src/Data/Container/Indexed/WithK.agda b/src/Data/Container/Indexed/WithK.agda index ca5f18205d..9897402264 100644 --- a/src/Data/Container/Indexed/WithK.agda +++ b/src/Data/Container/Indexed/WithK.agda @@ -15,7 +15,8 @@ module Data.Container.Indexed.WithK where open import Axiom.Extensionality.Heterogeneous using (Extensionality) open import Data.Container.Indexed hiding (module PlainMorphism) -open import Data.Product as Prod hiding (map) +open import Data.Product.Base + using (_,_; -,_; _×_; ∃; proj₁; proj₂; Σ-syntax) open import Function.Base renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_) open import Level open import Relation.Unary using (Pred; _⊆_) diff --git a/src/Data/Container/Morphism/Properties.agda b/src/Data/Container/Morphism/Properties.agda index fc71843263..c0d84007b4 100644 --- a/src/Data/Container/Morphism/Properties.agda +++ b/src/Data/Container/Morphism/Properties.agda @@ -10,7 +10,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 Data.Product.Base using (∃; proj₁; proj₂; _,_) open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_) diff --git a/src/Data/Container/Relation/Unary/All.agda b/src/Data/Container/Relation/Unary/All.agda index 65d593eea4..829bd3a0c9 100644 --- a/src/Data/Container/Relation/Unary/All.agda +++ b/src/Data/Container/Relation/Unary/All.agda @@ -10,7 +10,7 @@ module Data.Container.Relation.Unary.All where open import Level using (_⊔_) open import Relation.Unary using (Pred; _⊆_) -open import Data.Product as Prod using (_,_; proj₁; proj₂; ∃) +open import Data.Product.Base using (_,_; proj₁; proj₂; ∃) open import Function.Base using (_∘′_; id) open import Data.Container.Core hiding (map) diff --git a/src/Data/Container/Relation/Unary/Any.agda b/src/Data/Container/Relation/Unary/Any.agda index de3937f221..121391f4d6 100644 --- a/src/Data/Container/Relation/Unary/Any.agda +++ b/src/Data/Container/Relation/Unary/Any.agda @@ -10,7 +10,7 @@ module Data.Container.Relation.Unary.Any where open import Level using (_⊔_) open import Relation.Unary using (Pred; _⊆_) -open import Data.Product as Prod using (_,_; proj₂; ∃) +open import Data.Product.Base using (_,_; proj₂; ∃) open import Function.Base using (_∘′_; id) open import Data.Container.Core hiding (map) diff --git a/src/Data/Container/Relation/Unary/Any/Properties.agda b/src/Data/Container/Relation/Unary/Any/Properties.agda index ceae1510c9..d1d35c5a02 100644 --- a/src/Data/Container/Relation/Unary/Any/Properties.agda +++ b/src/Data/Container/Relation/Unary/Any/Properties.agda @@ -10,7 +10,7 @@ module Data.Container.Relation.Unary.Any.Properties where open import Level open import Algebra -open import Data.Product as Prod using (∃; _×_; ∃₂; _,_; proj₂) +open import Data.Product.Base using (∃; _×_; ∃₂; _,_; proj₂) open import Data.Product.Function.NonDependent.Propositional using (_×-cong_) import Data.Product.Function.Dependent.Propositional as Σ open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]) diff --git a/src/Data/Fin/Subset.agda b/src/Data/Fin/Subset.agda index 01926df438..b3d53106ff 100644 --- a/src/Data/Fin/Subset.agda +++ b/src/Data/Fin/Subset.agda @@ -13,7 +13,7 @@ open import Data.Bool using (not; _∧_; _∨_; _≟_) open import Data.Fin.Base using (Fin; zero; suc) open import Data.List.Base using (List; foldr; foldl) open import Data.Nat.Base using (ℕ) -open import Data.Product using (∃; _×_) +open import Data.Product.Base using (∃; _×_) open import Data.Vec.Base hiding (foldr; foldl) open import Relation.Nullary diff --git a/src/Data/Graph/Acyclic.agda b/src/Data/Graph/Acyclic.agda index 586b28e278..d40d078bd3 100644 --- a/src/Data/Graph/Acyclic.agda +++ b/src/Data/Graph/Acyclic.agda @@ -20,7 +20,7 @@ open import Data.Fin as Fin using (Fin; Fin′; zero; suc; #_; toℕ; _≟_; opposite) renaming (_ℕ-ℕ_ to _-_) import Data.Fin.Properties as FP import Data.Fin.Permutation.Components as PC -open import Data.Product as Prod using (∃; _×_; _,_) +open import Data.Product.Base as Prod using (∃; _×_; _,_) open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; decToMaybe) open import Data.Empty open import Data.Unit.Base using (⊤; tt) diff --git a/src/Data/List/Fresh/Membership/Setoid/Properties.agda b/src/Data/List/Fresh/Membership/Setoid/Properties.agda index e287147516..d2f2634bf8 100644 --- a/src/Data/List/Fresh/Membership/Setoid/Properties.agda +++ b/src/Data/List/Fresh/Membership/Setoid/Properties.agda @@ -15,7 +15,7 @@ open import Level using (Level; _⊔_) open import Data.Empty open import Data.Nat.Base open import Data.Nat.Properties -open import Data.Product using (∃; _×_; _,_) +open import Data.Product.Base using (∃; _×_; _,_) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; fromInj₂) open import Function.Base using (id; _∘′_; _$_) diff --git a/src/Data/List/Fresh/Relation/Unary/Any.agda b/src/Data/List/Fresh/Relation/Unary/Any.agda index 9c2050472c..dbb9dd0dec 100644 --- a/src/Data/List/Fresh/Relation/Unary/Any.agda +++ b/src/Data/List/Fresh/Relation/Unary/Any.agda @@ -10,7 +10,7 @@ module Data.List.Fresh.Relation.Unary.Any where open import Level using (Level; _⊔_; Lift) open import Data.Empty -open import Data.Product using (∃; _,_; -,_) +open import Data.Product.Base using (∃; _,_; -,_) open import Data.Sum.Base using (_⊎_; [_,_]′; inj₁; inj₂) open import Function.Bundles using (_⇔_; mk⇔) open import Relation.Nullary.Negation using (¬_) diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda index f781e1678d..dfef9fa160 100644 --- a/src/Data/List/Membership/Propositional/Properties.agda +++ b/src/Data/List/Membership/Propositional/Properties.agda @@ -22,7 +22,7 @@ open import Data.List.Relation.Binary.Equality.Propositional open import Data.List.Effectful using (monad) open import Data.Nat.Base using (ℕ; zero; suc; pred; s≤s; _≤_; _<_; _≤ᵇ_) open import Data.Nat.Properties -open import Data.Product hiding (map) +open import Data.Product.Base hiding (map) open import Data.Product.Function.NonDependent.Propositional using (_×-cong_) import Data.Product.Function.Dependent.Propositional as Σ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂) diff --git a/src/Data/List/Membership/Propositional/Properties/Core.agda b/src/Data/List/Membership/Propositional/Properties/Core.agda index 85ad85aab0..aec90ef8d1 100644 --- a/src/Data/List/Membership/Propositional/Properties/Core.agda +++ b/src/Data/List/Membership/Propositional/Properties/Core.agda @@ -17,7 +17,7 @@ open import Function.Inverse using (_↔_; inverse) open import Data.List.Base using (List) open import Data.List.Relation.Unary.Any as Any using (Any; here; there) open import Data.List.Membership.Propositional -open import Data.Product as Prod +open import Data.Product.Base as Prod using (_,_; proj₁; proj₂; uncurry′; ∃; _×_) open import Level using (Level) open import Relation.Binary.PropositionalEquality.Core as P diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda index 47768eed76..2fee07309f 100644 --- a/src/Data/List/Membership/Setoid/Properties.agda +++ b/src/Data/List/Membership/Setoid/Properties.agda @@ -20,7 +20,7 @@ import Data.List.Relation.Binary.Equality.Setoid as Equality import Data.List.Relation.Unary.Unique.Setoid as Unique open import Data.Nat.Base using (suc; z≤n; s≤s; _≤_; _<_) open import Data.Nat.Properties using (≤-trans; n≤1+n) -open import Data.Product as Prod using (∃; _×_; _,_ ; ∃₂; proj₁; proj₂) +open import Data.Product.Base as Prod using (∃; _×_; _,_ ; ∃₂; proj₁; proj₂) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) open import Function.Base using (_$_; flip; _∘_; _∘′_; id) diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda index ac88bd72ef..d48b3dae45 100644 --- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda +++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda @@ -23,7 +23,7 @@ open import Data.List.Relation.Binary.Subset.Propositional.Properties using (⊆-preorder) open import Data.List.Relation.Binary.Permutation.Propositional open import Data.List.Relation.Binary.Permutation.Propositional.Properties -open import Data.Product as Prod hiding (map) +open import Data.Product.Base as Prod hiding (map) import Data.Product.Function.Dependent.Propositional as Σ open import Data.Sum.Base as Sum hiding (map) open import Data.Sum.Properties hiding (map-cong) diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda index dc7e34db86..42430b90ea 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda @@ -21,7 +21,7 @@ open import Data.List.Relation.Unary.All using (All; []; _∷_) open import Data.List.Membership.Propositional open import Data.List.Membership.Propositional.Properties import Data.List.Properties as Lₚ -open import Data.Product using (_,_; _×_; ∃; ∃₂) +open import Data.Product.Base using (_,_; _×_; ∃; ∃₂) open import Function.Base using (_∘_; _⟨_⟩_) open import Function.Equality using (_⟨$⟩_) open import Function.Inverse as Inv using (inverse) diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda index e7d2b4039c..57233a7b2a 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda @@ -32,7 +32,7 @@ import Data.List.Properties as Lₚ open import Data.Nat hiding (_⊔_) open import Data.Nat.Induction open import Data.Nat.Properties -open import Data.Product using (_,_; _×_; ∃; ∃₂; proj₁; proj₂) +open import Data.Product.Base using (_,_; _×_; ∃; ∃₂; proj₁; proj₂) open import Function.Base using (_∘_; _⟨_⟩_; flip) open import Function.Equality using (_⟨$⟩_) open import Function.Inverse as Inv using (inverse) diff --git a/src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda b/src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda index 39d4439a86..75104bd39e 100644 --- a/src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda +++ b/src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda @@ -12,7 +12,7 @@ open import Level 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 Data.Product.Base using (∃; _×_; _,_; uncurry) open import Relation.Binary.Core using (REL; _⇒_) module _ {a b r} {A : Set a} {B : Set b} (R : REL A B r) where diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda index 7e7a3a090d..46d5d7d2cc 100644 --- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda @@ -24,7 +24,7 @@ open import Data.List.Relation.Binary.Sublist.Heterogeneous open import Data.Maybe.Relation.Unary.All as MAll using (nothing; just) open import Data.Nat.Base using (ℕ; _≤_; _≥_); open ℕ; open _≤_ import Data.Nat.Properties as ℕₚ -open import Data.Product using (∃₂; _×_; _,_; <_,_>; proj₂; uncurry) +open import Data.Product.Base using (∃₂; _×_; _,_; <_,_>; proj₂; uncurry) open import Function.Base open import Function.Bundles using (_⤖_; _⇔_ ; mk⤖; mk⇔) diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda index 1378e745f5..43df666804 100644 --- a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda @@ -19,7 +19,7 @@ open import Data.List.Relation.Binary.Sublist.Propositional hiding (map) import Data.List.Relation.Binary.Sublist.Setoid.Properties as SetoidProperties -open import Data.Product using (∃; _,_; proj₂) +open import Data.Product.Base using (∃; _,_; proj₂) open import Function.Base open import Level using (Level) open import Relation.Binary using (_Respects_) diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid.agda b/src/Data/List/Relation/Binary/Sublist/Setoid.agda index eff26de0aa..a07c6ffc25 100644 --- a/src/Data/List/Relation/Binary/Sublist/Setoid.agda +++ b/src/Data/List/Relation/Binary/Sublist/Setoid.agda @@ -24,7 +24,7 @@ import Data.List.Relation.Binary.Sublist.Heterogeneous.Core as HeterogeneousCore import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties as HeterogeneousProperties -open import Data.Product using (∃; ∃₂; _×_; _,_; proj₂) +open import Data.Product.Base using (∃; ∃₂; _×_; _,_; proj₂) open import Relation.Binary open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda index abe9a20b73..26303c1afc 100644 --- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda @@ -16,7 +16,7 @@ open import Data.List.Relation.Unary.Any using (Any) import Data.Maybe.Relation.Unary.All as Maybe open import Data.Nat.Base using (_≤_; _≥_) import Data.Nat.Properties as ℕₚ -open import Data.Product using (∃; _,_; proj₂) +open import Data.Product.Base using (∃; _,_; proj₂) open import Function.Base open import Function.Bundles using (_⇔_; _⤖_) open import Level diff --git a/src/Data/List/Relation/Ternary/Appending.agda b/src/Data/List/Relation/Ternary/Appending.agda index 1ae20e905f..1a2bab30e1 100644 --- a/src/Data/List/Relation/Ternary/Appending.agda +++ b/src/Data/List/Relation/Ternary/Appending.agda @@ -11,7 +11,7 @@ module Data.List.Relation.Ternary.Appending {a b c} {A : Set a} {B : Set b} {C : open import Level using (Level; _⊔_) open import Data.List.Base as List using (List; []; _∷_) open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_) -open import Data.Product as Prod using (∃₂; _×_; _,_; -,_) +open import Data.Product.Base using (∃₂; _×_; _,_; -,_) open import Relation.Binary.Core using (REL) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong) diff --git a/src/Data/List/Relation/Ternary/Interleaving.agda b/src/Data/List/Relation/Ternary/Interleaving.agda index 158701fc7e..8818638518 100644 --- a/src/Data/List/Relation/Ternary/Interleaving.agda +++ b/src/Data/List/Relation/Ternary/Interleaving.agda @@ -12,7 +12,7 @@ module Data.List.Relation.Ternary.Interleaving where open import Level open import Data.List.Base as List using (List; []; _∷_; _++_) open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_) -open import Data.Product as Prod using (∃; ∃₂; _×_; uncurry; _,_; -,_; proj₂) +open import Data.Product.Base as Prod using (∃; ∃₂; _×_; uncurry; _,_; -,_; proj₂) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Function.Base open import Relation.Binary diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda index 6a0020d269..8f3bcd640c 100644 --- a/src/Data/List/Relation/Unary/Any/Properties.agda +++ b/src/Data/List/Relation/Unary/Any/Properties.agda @@ -25,7 +25,7 @@ open import Data.Nat using (zero; suc; _<_; z; proj₁; proj₂; ∃₂; ∃) open import Data.Product.Function.NonDependent.Propositional open import Data.Sum.Base as Sum open import Data.Sum.Properties using (swap-involutive) diff --git a/src/Relation/Binary/Rewriting.agda b/src/Relation/Binary/Rewriting.agda index 9006765413..10d760e23b 100644 --- a/src/Relation/Binary/Rewriting.agda +++ b/src/Relation/Binary/Rewriting.agda @@ -10,7 +10,7 @@ module Relation.Binary.Rewriting where open import Agda.Builtin.Equality using (_≡_ ; refl) -open import Data.Product using (_×_ ; ∃ ; -,_; _,_ ; proj₁ ; proj₂) +open import Data.Product.Base using (_×_ ; ∃ ; -,_; _,_ ; proj₁ ; proj₂) open import Data.Empty open import Function.Base using (flip) open import Induction.WellFounded diff --git a/src/Relation/Unary/Indexed.agda b/src/Relation/Unary/Indexed.agda index 1acfdc8cef..d1cdbb01f5 100644 --- a/src/Relation/Unary/Indexed.agda +++ b/src/Relation/Unary/Indexed.agda @@ -8,7 +8,7 @@ module Relation.Unary.Indexed where -open import Data.Product using (∃; _×_) +open import Data.Product.Base using (∃; _×_) open import Level open import Relation.Nullary.Negation using (¬_) diff --git a/tests/data/trie/Main.agda b/tests/data/trie/Main.agda index 3ce2ad3ecb..8bd76616d2 100644 --- a/tests/data/trie/Main.agda +++ b/tests/data/trie/Main.agda @@ -12,7 +12,7 @@ import Data.Char.Properties as Char open import Data.List.Base as List using (List; []; _∷_) open import Data.List.Fresh as List# using (List#; []; _∷#_) open import Data.Maybe as Maybe -open import Data.Product as Prod +open import Data.Product.Base using (map₁) open import Data.String as String using (String; unlines; _++_) open import Data.These as These @@ -55,7 +55,7 @@ module _ {t} (L : Lexer t) where Keywords = Trie (const _ Tok) _ init : Keywords - init = fromList $ List.map (Prod.map₁ String.toList) $ proj₁ $ List#.toList keywords + init = fromList $ List.map (map₁ String.toList) $ proj₁ $ List#.toList keywords start : List Char → List Tok start = loop [] init From 490dcd6363479d8eafcd5655a15ae16f54187d6b Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Thu, 10 Aug 2023 15:52:43 -0400 Subject: [PATCH 3/5] Final changes --- README/Data/Trie/NonDependent.agda | 2 +- src/Data/Product/Instances.agda | 2 +- src/Data/Vec/Recursive/Properties.agda | 2 +- src/Foreign/Haskell/Coerce.agda | 2 +- src/Foreign/Haskell/Pair.agda | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/README/Data/Trie/NonDependent.agda b/README/Data/Trie/NonDependent.agda index 33e2126988..be2bd3811c 100644 --- a/README/Data/Trie/NonDependent.agda +++ b/README/Data/Trie/NonDependent.agda @@ -59,7 +59,7 @@ open import Data.Maybe as Maybe open import Data.Product.Base using (map₁; _×_; ∃; proj₁; _,_) open import Data.String.Base as String using (String) open import Data.String.Properties as String using (_≟_) -open import Data.These as These +open import Data.These as These hiding (map₁) open import Function.Base using (case_of_; _$_; _∘′_; id; _on_) open import Relation.Nary diff --git a/src/Data/Product/Instances.agda b/src/Data/Product/Instances.agda index 222a254b0b..93794c3c58 100644 --- a/src/Data/Product/Instances.agda +++ b/src/Data/Product/Instances.agda @@ -8,7 +8,7 @@ module Data.Product.Instances where -open import Data.Product +open import Data.Product.Base using (Σ) open import Data.Product.Properties open import Level diff --git a/src/Data/Vec/Recursive/Properties.agda b/src/Data/Vec/Recursive/Properties.agda index d557808cee..a449dbabd1 100644 --- a/src/Data/Vec/Recursive/Properties.agda +++ b/src/Data/Vec/Recursive/Properties.agda @@ -10,7 +10,7 @@ module Data.Vec.Recursive.Properties where open import Level using (Level) open import Data.Nat.Base hiding (_^_) -open import Data.Product +open import Data.Product.Base open import Data.Vec.Recursive open import Data.Vec.Base using (Vec; _∷_) open import Function.Inverse using (_↔_; inverse) diff --git a/src/Foreign/Haskell/Coerce.agda b/src/Foreign/Haskell/Coerce.agda index f593d10af3..3eb411c325 100644 --- a/src/Foreign/Haskell/Coerce.agda +++ b/src/Foreign/Haskell/Coerce.agda @@ -39,7 +39,7 @@ import IO.Primitive as STD import Data.List.Base as STD import Data.List.NonEmpty.Base as STD import Data.Maybe.Base as STD -import Data.Product as STD +import Data.Product.Base as STD import Data.Sum.Base as STD import Foreign.Haskell.Pair as FFI diff --git a/src/Foreign/Haskell/Pair.agda b/src/Foreign/Haskell/Pair.agda index 1f10b05169..84d4b8180b 100644 --- a/src/Foreign/Haskell/Pair.agda +++ b/src/Foreign/Haskell/Pair.agda @@ -9,7 +9,7 @@ module Foreign.Haskell.Pair where open import Level -open import Data.Product using (_×_; _,_) +open import Data.Product.Base using (_×_; _,_) private variable From 18a9d0d365f06e5cd892d1bcdc9a2ee89616e720 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Thu, 10 Aug 2023 16:00:51 -0400 Subject: [PATCH 4/5] Revert an import --- README/Data/Trie/NonDependent.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README/Data/Trie/NonDependent.agda b/README/Data/Trie/NonDependent.agda index be2bd3811c..0484e6005a 100644 --- a/README/Data/Trie/NonDependent.agda +++ b/README/Data/Trie/NonDependent.agda @@ -56,10 +56,10 @@ import Data.Char.Properties as Char open import Data.List.Base as List using (List; []; _∷_) open import Data.List.Fresh as List# using (List#; []; _∷#_) open import Data.Maybe as Maybe -open import Data.Product.Base using (map₁; _×_; ∃; proj₁; _,_) +open import Data.Product.Base as Prod using (_×_; ∃; proj₁; _,_) open import Data.String.Base as String using (String) open import Data.String.Properties as String using (_≟_) -open import Data.These as These hiding (map₁) +open import Data.These as These open import Function.Base using (case_of_; _$_; _∘′_; id; _on_) open import Relation.Nary @@ -127,7 +127,7 @@ module _ {t} (L : Lexer t) where -- characters one by one init : Keywords - init = fromList $ List.map (map₁ String.toList) $ proj₁ $ List#.toList keywords + init = fromList $ List.map (Prod.map₁ String.toList) $ proj₁ $ List#.toList keywords -- Kickstart the tokeniser with an empty accumulator and the initial -- trie. From b8b57816726d4223c3d469a54585057fc000acc2 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Thu, 10 Aug 2023 19:29:39 -0400 Subject: [PATCH 5/5] Revert golden test files --- tests/data/trie/Main.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/data/trie/Main.agda b/tests/data/trie/Main.agda index 8bd76616d2..3ce2ad3ecb 100644 --- a/tests/data/trie/Main.agda +++ b/tests/data/trie/Main.agda @@ -12,7 +12,7 @@ import Data.Char.Properties as Char open import Data.List.Base as List using (List; []; _∷_) open import Data.List.Fresh as List# using (List#; []; _∷#_) open import Data.Maybe as Maybe -open import Data.Product.Base using (map₁) +open import Data.Product as Prod open import Data.String as String using (String; unlines; _++_) open import Data.These as These @@ -55,7 +55,7 @@ module _ {t} (L : Lexer t) where Keywords = Trie (const _ Tok) _ init : Keywords - init = fromList $ List.map (map₁ String.toList) $ proj₁ $ List#.toList keywords + init = fromList $ List.map (Prod.map₁ String.toList) $ proj₁ $ List#.toList keywords start : List Char → List Tok start = loop [] init