From 1cd749a771ac878560a88a43faaf276ab47746ac Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Thu, 22 Jun 2023 15:29:26 -0400 Subject: [PATCH 1/3] Simplify more `Data.Product` import to `Data.Product.Base` --- src/Function/Bundles.agda | 2 +- src/Function/Construct/Identity.agda | 2 +- src/Function/Construct/Symmetry.agda | 2 +- src/Function/Endomorphism/Propositional.agda | 2 +- src/Function/Nary/NonDependent.agda | 2 +- src/Function/Nary/NonDependent/Base.agda | 2 +- src/Function/Properties/Bijection.agda | 2 +- src/Function/Properties/Inverse.agda | 2 +- src/Function/Related.agda | 2 +- src/Function/Related/TypeIsomorphisms/Solver.agda | 2 +- src/Reflection/AST/Abstraction.agda | 2 +- src/Reflection/AST/Argument.agda | 2 +- src/Reflection/AST/Definition.agda | 4 ++-- src/Reflection/AST/Show.agda | 2 +- src/Reflection/AST/Term.agda | 4 ++-- src/Reflection/AST/Traversal.agda | 12 ++++++------ src/Reflection/AST/Universe.agda | 2 +- src/Reflection/AnnotatedAST.agda | 2 +- src/Reflection/AnnotatedAST/Free.agda | 2 +- src/Reflection/External.agda | 2 +- src/Relation/Binary/Construct/NaturalOrder/Left.agda | 2 +- .../Binary/Construct/NaturalOrder/Right.agda | 2 +- src/Relation/Binary/Construct/Subst/Equality.agda | 2 +- src/Relation/Binary/Indexed/Homogeneous/Bundles.agda | 2 +- src/Relation/Binary/Indexed/Homogeneous/Core.agda | 2 +- .../Binary/Indexed/Homogeneous/Definitions.agda | 2 +- .../Binary/Indexed/Homogeneous/Structures.agda | 2 +- src/Relation/Binary/Lattice/Definitions.agda | 2 +- .../Binary/Lattice/Properties/BoundedLattice.agda | 2 +- .../Lattice/Properties/DistributiveLattice.agda | 2 +- src/Relation/Binary/Lattice/Properties/Lattice.agda | 2 +- src/Relation/Binary/Lattice/Structures.agda | 2 +- src/Relation/Binary/Morphism/Construct/Identity.agda | 2 +- src/Relation/Binary/Morphism/OrderMonomorphism.agda | 2 +- src/Relation/Binary/Morphism/Structures.agda | 2 +- src/Relation/Binary/Properties/HeytingAlgebra.agda | 2 +- 36 files changed, 43 insertions(+), 43 deletions(-) diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda index 6284182845..d113f14858 100644 --- a/src/Function/Bundles.agda +++ b/src/Function/Bundles.agda @@ -23,7 +23,7 @@ open import Function.Base using (_∘_) import Function.Definitions as FunctionDefinitions import Function.Structures as FunctionStructures open import Level using (Level; _⊔_; suc) -open import Data.Product using (_,_; proj₁; proj₂) +open import Data.Product.Base using (_,_; proj₁; proj₂) open import Relation.Binary hiding (_⇔_) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) diff --git a/src/Function/Construct/Identity.agda b/src/Function/Construct/Identity.agda index 1b69165dda..65556bced9 100644 --- a/src/Function/Construct/Identity.agda +++ b/src/Function/Construct/Identity.agda @@ -8,7 +8,7 @@ module Function.Construct.Identity where -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Function.Base using (id) open import Function.Bundles import Function.Definitions as Definitions diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda index ea86704a57..86fa273c57 100644 --- a/src/Function/Construct/Symmetry.agda +++ b/src/Function/Construct/Symmetry.agda @@ -8,7 +8,7 @@ module Function.Construct.Symmetry where -open import Data.Product using (_,_; swap; proj₁; proj₂) +open import Data.Product.Base using (_,_; swap; proj₁; proj₂) open import Function open import Level using (Level) open import Relation.Binary hiding (_⇔_) diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda index 8a78f69496..014fbc52cc 100644 --- a/src/Function/Endomorphism/Propositional.agda +++ b/src/Function/Endomorphism/Propositional.agda @@ -16,7 +16,7 @@ open import Algebra.Morphism; open Definitions open import Data.Nat.Base using (ℕ; zero; suc; _+_) open import Data.Nat.Properties using (+-0-monoid; +-semigroup) -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Function open import Function.Equality using (_⟨$⟩_) diff --git a/src/Function/Nary/NonDependent.agda b/src/Function/Nary/NonDependent.agda index 3c29079b5e..aa9c35a0f5 100644 --- a/src/Function/Nary/NonDependent.agda +++ b/src/Function/Nary/NonDependent.agda @@ -17,7 +17,7 @@ module Function.Nary.NonDependent where open import Level using (Level; 0ℓ; _⊔_; Lift) open import Data.Nat.Base using (ℕ; zero; suc) open import Data.Fin.Base using (Fin; zero; suc) -open import Data.Product using (_×_; _,_) +open import Data.Product.Base using (_×_; _,_) open import Data.Product.Nary.NonDependent open import Function.Base using (_∘′_; _$′_; const; flip) open import Relation.Unary using (IUniversal) diff --git a/src/Function/Nary/NonDependent/Base.agda b/src/Function/Nary/NonDependent/Base.agda index 72e093b3a7..efb24aec57 100644 --- a/src/Function/Nary/NonDependent/Base.agda +++ b/src/Function/Nary/NonDependent/Base.agda @@ -16,7 +16,7 @@ module Function.Nary.NonDependent.Base where open import Level using (Level; 0ℓ; _⊔_) open import Data.Nat.Base using (ℕ; zero; suc) -open import Data.Product using (_×_; _,_) +open import Data.Product.Base using (_×_; _,_) open import Data.Unit.Polymorphic.Base open import Function.Base using (_∘′_; _$′_; const; flip) diff --git a/src/Function/Properties/Bijection.agda b/src/Function/Properties/Bijection.agda index e484098774..1e458e958d 100644 --- a/src/Function/Properties/Bijection.agda +++ b/src/Function/Properties/Bijection.agda @@ -13,7 +13,7 @@ open import Level using (Level) open import Relation.Binary hiding (_⇔_) open import Relation.Binary.PropositionalEquality as P using (setoid) import Relation.Binary.Reasoning.Setoid as SetoidReasoning -open import Data.Product using (_,_; proj₁; proj₂) +open import Data.Product.Base using (_,_; proj₁; proj₂) open import Function.Base using (_∘_) open import Function.Properties.Inverse using (Inverse⇒Equivalence) diff --git a/src/Function/Properties/Inverse.agda b/src/Function/Properties/Inverse.agda index 6310a8479f..508a8664be 100644 --- a/src/Function/Properties/Inverse.agda +++ b/src/Function/Properties/Inverse.agda @@ -10,7 +10,7 @@ module Function.Properties.Inverse where open import Axiom.Extensionality.Propositional using (Extensionality) -open import Data.Product using (_,_; proj₁; proj₂) +open import Data.Product.Base using (_,_; proj₁; proj₂) open import Function.Bundles open import Level using (Level) open import Relation.Binary using (Setoid; IsEquivalence) diff --git a/src/Function/Related.agda b/src/Function/Related.agda index fa114d077c..ae1ead1f20 100644 --- a/src/Function/Related.agda +++ b/src/Function/Related.agda @@ -19,7 +19,7 @@ open import Function.LeftInverse as LeftInv using (LeftInverse) open import Function.Surjection as Surj using (Surjection) open import Relation.Binary open import Relation.Binary.PropositionalEquality as P using (_≡_) -open import Data.Product using (_,_; proj₁; proj₂; <_,_>) +open import Data.Product.Base using (_,_; proj₁; proj₂; <_,_>) import Function.Related.Propositional as R import Function.Bundles as B diff --git a/src/Function/Related/TypeIsomorphisms/Solver.agda b/src/Function/Related/TypeIsomorphisms/Solver.agda index 29f19c8afd..52f27d15ed 100644 --- a/src/Function/Related/TypeIsomorphisms/Solver.agda +++ b/src/Function/Related/TypeIsomorphisms/Solver.agda @@ -13,7 +13,7 @@ module Function.Related.TypeIsomorphisms.Solver where open import Algebra using (CommutativeSemiring) import Algebra.Solver.Ring.NaturalCoefficients.Default open import Data.Empty.Polymorphic using (⊥) -open import Data.Product using (_×_) +open import Data.Product.Base using (_×_) open import Data.Sum.Base using (_⊎_) open import Data.Unit.Polymorphic using (⊤) open import Level using (Level) diff --git a/src/Reflection/AST/Abstraction.agda b/src/Reflection/AST/Abstraction.agda index 9ed64b8835..0f726ee955 100644 --- a/src/Reflection/AST/Abstraction.agda +++ b/src/Reflection/AST/Abstraction.agda @@ -8,7 +8,7 @@ module Reflection.AST.Abstraction where -open import Data.Product using (_×_; <_,_>; uncurry) +open import Data.Product.Base using (_×_; <_,_>; uncurry) open import Data.String as String using (String) open import Level open import Relation.Nullary.Decidable using (Dec; map′; _×-dec_) diff --git a/src/Reflection/AST/Argument.agda b/src/Reflection/AST/Argument.agda index 1b0884b615..77e50b2774 100644 --- a/src/Reflection/AST/Argument.agda +++ b/src/Reflection/AST/Argument.agda @@ -9,7 +9,7 @@ module Reflection.AST.Argument where open import Data.List.Base as List using (List; []; _∷_) -open import Data.Product using (_×_; <_,_>; uncurry) +open import Data.Product.Base using (_×_; <_,_>; uncurry) open import Relation.Nullary.Decidable using (Dec; map′; _×-dec_) open import Relation.Binary using (DecidableEquality) open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong₂) diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda index 5b6dace7cd..c52cdf90c0 100644 --- a/src/Reflection/AST/Definition.agda +++ b/src/Reflection/AST/Definition.agda @@ -9,8 +9,8 @@ module Reflection.AST.Definition where import Data.List.Properties as Listₚ using (≡-dec) -import Data.Nat.Properties as ℕₚ using (_≟_) -open import Data.Product using (_×_; <_,_>; uncurry) +import Data.Nat.Properties as ℕₚ using (_≟_) +open import Data.Product.Base using (_×_; <_,_>; uncurry) open import Relation.Nullary.Decidable using (map′; _×-dec_; yes; no) open import Relation.Binary using (DecidableEquality) open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂) diff --git a/src/Reflection/AST/Show.agda b/src/Reflection/AST/Show.agda index ffe97352f4..70c7b4c161 100644 --- a/src/Reflection/AST/Show.agda +++ b/src/Reflection/AST/Show.agda @@ -15,7 +15,7 @@ import Data.Char as Char using (show) import Data.Float as Float using (show) open import Data.List hiding (_++_; intersperse) import Data.Nat.Show as ℕ using (show) -open import Data.Product using (_×_; _,_) +open import Data.Product.Base using (_×_; _,_) open import Data.String as String using (String; _++_; intersperse; braces; parens; parensIfSpace; _<+>_) import Data.Word as Word using (toℕ) diff --git a/src/Reflection/AST/Term.agda b/src/Reflection/AST/Term.agda index 183f839015..107075cf28 100644 --- a/src/Reflection/AST/Term.agda +++ b/src/Reflection/AST/Term.agda @@ -10,8 +10,8 @@ module Reflection.AST.Term where open import Data.List.Base as List hiding (_++_) open import Data.List.Properties using (∷-dec) -open import Data.Nat as ℕ using (ℕ; zero; suc) -open import Data.Product using (_×_; _,_; <_,_>; uncurry; map₁) +open import Data.Nat as ℕ using (ℕ; zero; suc) +open import Data.Product.Base using (_×_; _,_; <_,_>; uncurry; map₁) open import Data.Product.Properties using (,-injective) open import Data.Maybe.Base using (Maybe; just; nothing) open import Data.String as String using (String) diff --git a/src/Reflection/AST/Traversal.agda b/src/Reflection/AST/Traversal.agda index de28c8db2a..937a189aca 100644 --- a/src/Reflection/AST/Traversal.agda +++ b/src/Reflection/AST/Traversal.agda @@ -11,12 +11,12 @@ open import Effect.Applicative using (RawApplicative) module Reflection.AST.Traversal {F : Set → Set} (AppF : RawApplicative F) where -open import Data.Nat using (ℕ; zero; suc; _+_) -open import Data.List using (List; []; _∷_; _++_; reverse; length) -open import Data.Product using (_×_; _,_) -open import Data.String using (String) -open import Function using (_∘_) -open import Reflection hiding (pure) +open import Data.Nat using (ℕ; zero; suc; _+_) +open import Data.List using (List; []; _∷_; _++_; reverse; length) +open import Data.Product.Base using (_×_; _,_) +open import Data.String using (String) +open import Function using (_∘_) +open import Reflection hiding (pure) open RawApplicative AppF diff --git a/src/Reflection/AST/Universe.agda b/src/Reflection/AST/Universe.agda index 334458ce2d..dac0af71ed 100644 --- a/src/Reflection/AST/Universe.agda +++ b/src/Reflection/AST/Universe.agda @@ -10,7 +10,7 @@ module Reflection.AST.Universe where open import Data.List.Base using (List) open import Data.String.Base using (String) -open import Data.Product using (_×_) +open import Data.Product.Base using (_×_) open import Reflection.AST.Argument using (Arg) open import Reflection.AST.Abstraction using (Abs) open import Reflection.AST.Term using (Term; Pattern; Sort; Clause) diff --git a/src/Reflection/AnnotatedAST.agda b/src/Reflection/AnnotatedAST.agda index 61d55def7d..94ed93b628 100644 --- a/src/Reflection/AnnotatedAST.agda +++ b/src/Reflection/AnnotatedAST.agda @@ -17,7 +17,7 @@ open import Effect.Applicative using (RawApplicative) open import Data.Bool.Base using (Bool; false; true; if_then_else_) open import Data.List.Base using (List; []; _∷_) open import Data.List.Relation.Unary.All using (All; _∷_; []) -open import Data.Product using (_×_; _,_; proj₁; proj₂) +open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) open import Data.String.Base using (String) open import Reflection hiding (pure) diff --git a/src/Reflection/AnnotatedAST/Free.agda b/src/Reflection/AnnotatedAST/Free.agda index 79ae7a96be..2017e2fd9f 100644 --- a/src/Reflection/AnnotatedAST/Free.agda +++ b/src/Reflection/AnnotatedAST/Free.agda @@ -12,7 +12,7 @@ open import Data.Bool.Base using (if_then_else_) open import Data.Nat.Base using (ℕ; _∸_; compare; _<ᵇ_; less; equal; greater) open import Data.List.Base using (List; []; _∷_; [_]; concatMap; length) open import Data.List.Relation.Unary.All using (_∷_) -open import Data.Product using (_×_; _,_; proj₁; proj₂) +open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) open import Data.String.Base using (String) open import Reflection diff --git a/src/Reflection/External.agda b/src/Reflection/External.agda index 3206ee2145..965067ebc3 100644 --- a/src/Reflection/External.agda +++ b/src/Reflection/External.agda @@ -12,7 +12,7 @@ import Agda.Builtin.Reflection.External as Builtin open import Data.Nat.Base using (ℕ; suc; zero; NonZero) open import Data.List.Base using (List; _∷_; []) -open import Data.Product using (_×_; _,_) +open import Data.Product.Base using (_×_; _,_) open import Data.String.Base as String using (String; _++_) open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]) open import Data.Unit.Base using (⊤; tt) diff --git a/src/Relation/Binary/Construct/NaturalOrder/Left.agda b/src/Relation/Binary/Construct/NaturalOrder/Left.agda index db1d0f5aff..e0ab59e9ca 100644 --- a/src/Relation/Binary/Construct/NaturalOrder/Left.agda +++ b/src/Relation/Binary/Construct/NaturalOrder/Left.agda @@ -8,7 +8,7 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra.Core -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/Relation/Binary/Construct/NaturalOrder/Right.agda b/src/Relation/Binary/Construct/NaturalOrder/Right.agda index 7c4a6ab119..5278f0b116 100644 --- a/src/Relation/Binary/Construct/NaturalOrder/Right.agda +++ b/src/Relation/Binary/Construct/NaturalOrder/Right.agda @@ -8,7 +8,7 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra.Core using (Op₂) -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/Relation/Binary/Construct/Subst/Equality.agda b/src/Relation/Binary/Construct/Subst/Equality.agda index 4e0a3d0100..24e465f9f0 100644 --- a/src/Relation/Binary/Construct/Subst/Equality.agda +++ b/src/Relation/Binary/Construct/Subst/Equality.agda @@ -9,7 +9,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Data.Product as Prod +open import Data.Product.Base as Prod open import Relation.Binary module Relation.Binary.Construct.Subst.Equality diff --git a/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda b/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda index 670949c138..90d81e9b4a 100644 --- a/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda +++ b/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda @@ -11,7 +11,7 @@ module Relation.Binary.Indexed.Homogeneous.Bundles where -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Function.Base using (_⟨_⟩_) open import Level using (Level; _⊔_; suc) open import Relation.Binary as B using (_⇒_) diff --git a/src/Relation/Binary/Indexed/Homogeneous/Core.agda b/src/Relation/Binary/Indexed/Homogeneous/Core.agda index 6dc2e03f82..4483bd7e82 100644 --- a/src/Relation/Binary/Indexed/Homogeneous/Core.agda +++ b/src/Relation/Binary/Indexed/Homogeneous/Core.agda @@ -12,7 +12,7 @@ module Relation.Binary.Indexed.Homogeneous.Core where open import Level using (Level; _⊔_) -open import Data.Product using (_×_) +open import Data.Product.Base using (_×_) open import Relation.Binary as B using (REL; Rel) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) import Relation.Binary.Indexed.Heterogeneous as I diff --git a/src/Relation/Binary/Indexed/Homogeneous/Definitions.agda b/src/Relation/Binary/Indexed/Homogeneous/Definitions.agda index 0231def44f..6160c7e014 100644 --- a/src/Relation/Binary/Indexed/Homogeneous/Definitions.agda +++ b/src/Relation/Binary/Indexed/Homogeneous/Definitions.agda @@ -11,7 +11,7 @@ module Relation.Binary.Indexed.Homogeneous.Definitions where -open import Data.Product using (_×_) +open import Data.Product.Base using (_×_) open import Level using (Level) import Relation.Binary as B open import Relation.Unary.Indexed using (IPred) diff --git a/src/Relation/Binary/Indexed/Homogeneous/Structures.agda b/src/Relation/Binary/Indexed/Homogeneous/Structures.agda index 1404bf7f52..eb46c0356e 100644 --- a/src/Relation/Binary/Indexed/Homogeneous/Structures.agda +++ b/src/Relation/Binary/Indexed/Homogeneous/Structures.agda @@ -17,7 +17,7 @@ module Relation.Binary.Indexed.Homogeneous.Structures (_≈ᵢ_ : IRel A ℓ) -- The underlying indexed equality relation where -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Function.Base using (_⟨_⟩_) open import Level using (Level; _⊔_; suc) open import Relation.Binary as B using (_⇒_) diff --git a/src/Relation/Binary/Lattice/Definitions.agda b/src/Relation/Binary/Lattice/Definitions.agda index 61102f19f9..00c0003adb 100644 --- a/src/Relation/Binary/Lattice/Definitions.agda +++ b/src/Relation/Binary/Lattice/Definitions.agda @@ -12,7 +12,7 @@ module Relation.Binary.Lattice.Definitions where open import Algebra.Core -open import Data.Product using (_×_; _,_) +open import Data.Product.Base using (_×_; _,_) open import Function.Base using (flip) open import Relation.Binary open import Level diff --git a/src/Relation/Binary/Lattice/Properties/BoundedLattice.agda b/src/Relation/Binary/Lattice/Properties/BoundedLattice.agda index 95bf238945..dfed059015 100644 --- a/src/Relation/Binary/Lattice/Properties/BoundedLattice.agda +++ b/src/Relation/Binary/Lattice/Properties/BoundedLattice.agda @@ -14,7 +14,7 @@ module Relation.Binary.Lattice.Properties.BoundedLattice open BoundedLattice L open import Algebra.Definitions _≈_ -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Relation.Binary using (Setoid) open import Relation.Binary.Lattice.Properties.MeetSemilattice meetSemilattice open import Relation.Binary.Lattice.Properties.JoinSemilattice joinSemilattice diff --git a/src/Relation/Binary/Lattice/Properties/DistributiveLattice.agda b/src/Relation/Binary/Lattice/Properties/DistributiveLattice.agda index 8ee0462d39..e3bd0170eb 100644 --- a/src/Relation/Binary/Lattice/Properties/DistributiveLattice.agda +++ b/src/Relation/Binary/Lattice/Properties/DistributiveLattice.agda @@ -14,7 +14,7 @@ module Relation.Binary.Lattice.Properties.DistributiveLattice open DistributiveLattice L hiding (refl) open import Algebra.Definitions _≈_ -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Relation.Binary open import Relation.Binary.Reasoning.Setoid setoid open import Relation.Binary.Lattice.Properties.Lattice lattice diff --git a/src/Relation/Binary/Lattice/Properties/Lattice.agda b/src/Relation/Binary/Lattice/Properties/Lattice.agda index a221c35b2e..633832a26c 100644 --- a/src/Relation/Binary/Lattice/Properties/Lattice.agda +++ b/src/Relation/Binary/Lattice/Properties/Lattice.agda @@ -16,7 +16,7 @@ open Lattice L import Algebra.Lattice as Alg import Algebra.Structures as Alg open import Algebra.Definitions _≈_ -open import Data.Product using (_,_) +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/Structures.agda b/src/Relation/Binary/Lattice/Structures.agda index 10178af05d..07dbfad6a5 100644 --- a/src/Relation/Binary/Lattice/Structures.agda +++ b/src/Relation/Binary/Lattice/Structures.agda @@ -19,7 +19,7 @@ module Relation.Binary.Lattice.Structures open import Algebra.Core open import Algebra.Definitions -open import Data.Product using (_×_; _,_) +open import Data.Product.Base using (_×_; _,_) open import Level using (suc; _⊔_) open import Relation.Binary.Lattice.Definitions diff --git a/src/Relation/Binary/Morphism/Construct/Identity.agda b/src/Relation/Binary/Morphism/Construct/Identity.agda index c8ed9c6b03..db12c9793b 100644 --- a/src/Relation/Binary/Morphism/Construct/Identity.agda +++ b/src/Relation/Binary/Morphism/Construct/Identity.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Function.Base using (id) open import Level using (Level) open import Relation.Binary diff --git a/src/Relation/Binary/Morphism/OrderMonomorphism.agda b/src/Relation/Binary/Morphism/OrderMonomorphism.agda index dd2e0ef821..3d788184c2 100644 --- a/src/Relation/Binary/Morphism/OrderMonomorphism.agda +++ b/src/Relation/Binary/Morphism/OrderMonomorphism.agda @@ -11,7 +11,7 @@ open import Algebra.Morphism.Definitions open import Function.Base -open import Data.Product using (_,_; map) +open import Data.Product.Base using (_,_; map) open import Relation.Binary open import Relation.Binary.Morphism import Relation.Binary.Morphism.RelMonomorphism as RawRelation diff --git a/src/Relation/Binary/Morphism/Structures.agda b/src/Relation/Binary/Morphism/Structures.agda index 39a333e1b7..f1fba75607 100644 --- a/src/Relation/Binary/Morphism/Structures.agda +++ b/src/Relation/Binary/Morphism/Structures.agda @@ -12,7 +12,7 @@ module Relation.Binary.Morphism.Structures {a b} {A : Set a} {B : Set b} where -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Function.Definitions open import Level open import Relation.Binary.Morphism.Definitions A B diff --git a/src/Relation/Binary/Properties/HeytingAlgebra.agda b/src/Relation/Binary/Properties/HeytingAlgebra.agda index f823a5b519..8786792e78 100644 --- a/src/Relation/Binary/Properties/HeytingAlgebra.agda +++ b/src/Relation/Binary/Properties/HeytingAlgebra.agda @@ -15,7 +15,7 @@ open HeytingAlgebra L open import Algebra.Core open import Algebra.Definitions _≈_ -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Function.Base using (_$_; flip; _∘_) open import Level using (_⊔_) open import Relation.Binary From c45603685710bd99b0b25ff97b95d4843da59207 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Thu, 22 Jun 2023 14:14:26 -0400 Subject: [PATCH 2/3] Simplify more `Data.Product` import to `Data.Product.Base` --- src/Relation/Nary.agda | 2 +- src/Relation/Nullary/Universe.agda | 2 +- src/Relation/Unary/Algebra.agda | 2 +- src/System/Environment.agda | 2 +- src/System/FilePath/Posix.agda | 2 +- src/System/Process.agda | 2 +- src/Tactic/MonoidSolver.agda | 2 +- .../RingSolver/Core/Polynomial/Homomorphism/Addition.agda | 2 +- .../RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda | 2 +- src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda | 2 +- .../RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda | 2 +- .../RingSolver/Core/Polynomial/Homomorphism/Negation.agda | 2 +- .../RingSolver/Core/Polynomial/Homomorphism/Variables.agda | 2 +- src/Tactic/RingSolver/Core/Polynomial/Semantics.agda | 2 +- src/Test/Golden.agda | 2 +- src/Text/Regex/Properties/Core.agda | 2 +- src/Text/Tabular/List.agda | 2 +- src/Text/Tabular/Vec.agda | 2 +- 18 files changed, 18 insertions(+), 18 deletions(-) diff --git a/src/Relation/Nary.agda b/src/Relation/Nary.agda index da804883f5..36d1db0568 100644 --- a/src/Relation/Nary.agda +++ b/src/Relation/Nary.agda @@ -19,7 +19,7 @@ open import Data.Unit.Base open import Data.Bool.Base using (true; false) open import Data.Empty open import Data.Nat.Base using (zero; suc) -open import Data.Product as Prod using (_×_; _,_) +open import Data.Product.Base as Prod using (_×_; _,_) open import Data.Product.Nary.NonDependent open import Data.Sum.Base using (_⊎_) open import Function.Base using (_$_; _∘′_) diff --git a/src/Relation/Nullary/Universe.agda b/src/Relation/Nullary/Universe.agda index 5df3c1c423..658f8c7bf7 100644 --- a/src/Relation/Nullary/Universe.agda +++ b/src/Relation/Nullary/Universe.agda @@ -19,7 +19,7 @@ import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial as Trivial open import Data.Sum.Base as Sum hiding (map) open import Data.Sum.Relation.Binary.Pointwise -open import Data.Product as Prod hiding (map) +open import Data.Product.Base as Prod hiding (map) open import Data.Product.Relation.Binary.Pointwise.NonDependent open import Function.Base using (_∘_; id) import Function.Equality as FunS diff --git a/src/Relation/Unary/Algebra.agda b/src/Relation/Unary/Algebra.agda index 600bab6c1f..514470de38 100644 --- a/src/Relation/Unary/Algebra.agda +++ b/src/Relation/Unary/Algebra.agda @@ -14,7 +14,7 @@ open import Algebra.Lattice.Bundles import Algebra.Lattice.Structures as AlgebraicLatticeStructures import Algebra.Structures as AlgebraicStructures open import Data.Empty.Polymorphic using (⊥-elim) -open import Data.Product as Product using (_,_; proj₁; proj₂; <_,_>; curry; uncurry) +open import Data.Product.Base as Product using (_,_; proj₁; proj₂; <_,_>; curry; uncurry) open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]) open import Data.Unit.Polymorphic using (tt) open import Function.Base using (id; const; _∘_) diff --git a/src/System/Environment.agda b/src/System/Environment.agda index 228bf699ac..ec6833f64c 100644 --- a/src/System/Environment.agda +++ b/src/System/Environment.agda @@ -11,7 +11,7 @@ module System.Environment where open import IO using (IO; lift; run; ignore) open import Data.List.Base using (List) open import Data.Maybe.Base using (Maybe) -open import Data.Product using (_×_) +open import Data.Product.Base using (_×_) open import Data.String.Base using (String) open import Data.Unit.Polymorphic using (⊤) open import Foreign.Haskell.Coerce diff --git a/src/System/FilePath/Posix.agda b/src/System/FilePath/Posix.agda index d486f1d342..f12cf8180e 100644 --- a/src/System/FilePath/Posix.agda +++ b/src/System/FilePath/Posix.agda @@ -13,7 +13,7 @@ open import Agda.Builtin.List using (List) open import Agda.Builtin.String using (String) open import IO.Base using (IO; lift) open import Data.Maybe.Base using (Maybe) -open import Data.Product using (_×_) +open import Data.Product.Base using (_×_) open import Data.Sum.Base using (_⊎_) open import Foreign.Haskell.Coerce diff --git a/src/System/Process.agda b/src/System/Process.agda index 1473788365..4aff9ca4dd 100644 --- a/src/System/Process.agda +++ b/src/System/Process.agda @@ -10,7 +10,7 @@ module System.Process where open import Level using (Level) open import Data.List.Base using (List) -open import Data.Product using (_×_; proj₁) +open import Data.Product.Base using (_×_; proj₁) open import Data.String.Base using (String) open import Data.Unit.Polymorphic using (⊤) open import Foreign.Haskell.Coerce diff --git a/src/Tactic/MonoidSolver.agda b/src/Tactic/MonoidSolver.agda index 991ff41556..1448e41fe3 100644 --- a/src/Tactic/MonoidSolver.agda +++ b/src/Tactic/MonoidSolver.agda @@ -79,7 +79,7 @@ open import Data.Bool as Bool using (Bool; _∨_; if_then_else_) open import Data.Maybe as Maybe using (Maybe; just; nothing; maybe) open import Data.List.Base as List using (List; _∷_; []) open import Data.Nat as ℕ using (ℕ; suc; zero) -open import Data.Product as Product using (_×_; _,_) +open import Data.Product.Base as Product using (_×_; _,_) open import Reflection.AST open import Reflection.AST.Term diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda index 1f6de95f4f..3ea01b2c17 100644 --- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda +++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda @@ -15,7 +15,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Addition open import Data.Nat as ℕ using (ℕ; suc; zero; compare; _≤′_; ≤′-step; ≤′-refl) open import Data.Nat.Properties as ℕₚ using (≤′-trans) -open import Data.Product using (_,_; _×_; proj₂) +open import Data.Product.Base using (_,_; _×_; proj₂) open import Data.List.Base using (_∷_; []) open import Data.List.Kleene open import Data.Vec using (Vec) diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda index 9435251957..eeacadb154 100644 --- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda +++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda @@ -16,7 +16,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Exponentiation open import Function.Base using (_⟨_⟩_) open import Data.Nat.Base as ℕ using (ℕ; suc; zero; compare) -open import Data.Product using (_,_; _×_; proj₁; proj₂) +open import Data.Product.Base using (_,_; _×_; proj₁; proj₂) open import Data.List.Kleene open import Data.Vec using (Vec) diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda index 3e1ce2bfe3..90183bc4c9 100644 --- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda +++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda @@ -21,7 +21,7 @@ open import Data.Fin using (Fin; zero; su open import Data.List.Base using (_∷_; []) open import Data.Unit using (tt) open import Data.List.Kleene -open import Data.Product using (_,_; proj₁; proj₂; map₁; _×_) +open import Data.Product.Base using (_,_; proj₁; proj₂; map₁; _×_) open import Data.Maybe using (nothing; just) open import Function.Base using (_⟨_⟩_) open import Level using (lift) diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda index 2baeac0f23..c7ad6d6145 100644 --- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda +++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda @@ -16,7 +16,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Multiplication open import Data.Nat.Base as ℕ using (ℕ; suc; zero; _<′_; _≤′_; ≤′-step; ≤′-refl) open import Data.Nat.Properties using (≤′-trans) open import Data.Nat.Induction -open import Data.Product using (_×_; _,_; proj₁; proj₂; map₁) +open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; map₁) open import Data.List.Kleene open import Data.Vec using (Vec) open import Function.Base using (_⟨_⟩_; flip) diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda index dd84eafef2..59b99cf71b 100644 --- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda +++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda @@ -13,7 +13,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Negation (homo : Homomorphism r₁ r₂ r₃ r₄) where -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Data.Vec using (Vec) open import Data.Nat using (_<′_) open import Data.Nat.Induction diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Variables.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Variables.agda index c3884e9e2a..9fcaca2f66 100644 --- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Variables.agda +++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Variables.agda @@ -13,7 +13,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Variables (homo : Homomorphism r₁ r₂ r₃ r₄) where -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Data.Vec.Base as Vec using (Vec) open import Data.Fin using (Fin) open import Data.List.Kleene diff --git a/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda b/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda index 8cde662620..26e19d428a 100644 --- a/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda +++ b/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda @@ -16,7 +16,7 @@ module Tactic.RingSolver.Core.Polynomial.Semantics open import Data.Nat using (ℕ; suc; zero; _≤′_; ≤′-step; ≤′-refl) open import Data.Vec using (Vec; []; _∷_; uncons) open import Data.List.Base using ([]; _∷_) -open import Data.Product using (_,_; _×_) +open import Data.Product.Base using (_,_; _×_) open import Data.List.Kleene using (_+; _*; ∹_; _&_; []) open Homomorphism homo hiding (_^_) diff --git a/src/Test/Golden.agda b/src/Test/Golden.agda index efbfc59ada..079e25720a 100644 --- a/src/Test/Golden.agda +++ b/src/Test/Golden.agda @@ -89,7 +89,7 @@ open import Data.List.Relation.Unary.Any using (any?) open import Data.Maybe.Base using (Maybe; just; nothing; fromMaybe) open import Data.Nat.Base using (ℕ; _≡ᵇ_; _<ᵇ_; _+_; _∸_) import Data.Nat.Show as ℕ using (show) -open import Data.Product using (_×_; _,_) +open import Data.Product.Base using (_×_; _,_) open import Data.String as String using (String; lines; unlines; unwords; concat; _≟_) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Data.Unit.Base using (⊤) diff --git a/src/Text/Regex/Properties/Core.agda b/src/Text/Regex/Properties/Core.agda index e1916fb5cf..51097a7656 100644 --- a/src/Text/Regex/Properties/Core.agda +++ b/src/Text/Regex/Properties/Core.agda @@ -17,7 +17,7 @@ open import Data.List.Base as List using (List; []; _∷_; _++_) open import Data.List.Relation.Unary.Any using (Any; here; there) open import Data.List.Relation.Unary.All using (All; []; _∷_) -open import Data.Product using (_×_; _,_) +open import Data.Product.Base using (_×_; _,_) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Relation.Nullary using (¬_; Dec; yes; no) diff --git a/src/Text/Tabular/List.agda b/src/Text/Tabular/List.agda index dd06ea809a..70fc09f3d5 100644 --- a/src/Text/Tabular/List.agda +++ b/src/Text/Tabular/List.agda @@ -11,7 +11,7 @@ module Text.Tabular.List where open import Data.String using (String) open import Data.List.Base import Data.Nat.Properties as ℕₚ -open import Data.Product using (-,_; proj₂) +open import Data.Product.Base using (-,_; proj₂) open import Data.Vec.Base as Vec using (Vec) open import Data.Vec.Bounded.Base as Vec≤ using (Vec≤) open import Function.Base diff --git a/src/Text/Tabular/Vec.agda b/src/Text/Tabular/Vec.agda index 74f899905c..1286ab1e14 100644 --- a/src/Text/Tabular/Vec.agda +++ b/src/Text/Tabular/Vec.agda @@ -9,7 +9,7 @@ module Text.Tabular.Vec where open import Data.List.Base using (List) -open import Data.Product as Prod using (uncurry) +open import Data.Product.Base as Prod using (uncurry) open import Data.String using (String; rectangle; fromAlignment) open import Data.Vec.Base open import Function.Base From 5bb1eb44d41c4f8b6c22b3fa77d8426694c55a3b Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Fri, 28 Jul 2023 17:28:43 -0400 Subject: [PATCH 3/3] Indent --- src/Reflection/AST/Abstraction.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Reflection/AST/Abstraction.agda b/src/Reflection/AST/Abstraction.agda index 75c05ca51e..55043355d7 100644 --- a/src/Reflection/AST/Abstraction.agda +++ b/src/Reflection/AST/Abstraction.agda @@ -8,7 +8,7 @@ module Reflection.AST.Abstraction where -open import Data.Product.Base using (_×_; <_,_>; uncurry) +open import Data.Product.Base using (_×_; <_,_>; uncurry) open import Data.String as String using (String) open import Level open import Relation.Nullary.Decidable using (Dec; map′; _×-dec_)