[Import] Data.List

jmougeot · jmougeot · commit f6408359c292 · 2025-02-26T12:15:48.000-05:00
diff --git a/src/Data/List/Membership/DecPropositional.agda b/src/Data/List/Membership/DecPropositional.agda
@@ -13,8 +13,6 @@ module Data.List.Membership.DecPropositional
 
 open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 
-open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
-
 ------------------------------------------------------------------------
 -- Re-export contents of propositional membership
 
diff --git a/src/Data/List/Membership/Propositional/Properties/Core.agda b/src/Data/List/Membership/Propositional/Properties/Core.agda
@@ -13,7 +13,7 @@
 module Data.List.Membership.Propositional.Properties.Core where
 
 open import Data.List.Base using (List; [])
-open import Data.List.Membership.Propositional
+open import Data.List.Membership.Propositional using (_∈_; _∉_; find; lose)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.Product.Base as Product using (_,_; ∃; _×_)
 open import Function.Base using (flip; id; _∘_)
diff --git a/src/Data/List/Membership/Propositional/Properties/WithK.agda b/src/Data/List/Membership/Propositional/Properties/WithK.agda
@@ -9,14 +9,15 @@
 
 module Data.List.Membership.Propositional.Properties.WithK where
 
-open import Level using (Level)
-open import Function.Bundles using (Equivalence)
-open import Data.List.Base
-open import Data.List.Relation.Unary.Unique.Propositional
-open import Data.List.Membership.Propositional
+open import Data.List.Base using (List; []; _∷_)
+open import Data.List.Relation.Unary.Unique.Propositional using (Unique)
+open import Data.List.Membership.Propositional using (_∈_; _∉_)
 import Data.List.Membership.Setoid.Properties as Membership
+  using (unique⇒irrelevant)
 open import Data.List.Relation.Binary.BagAndSetEquality using (_∼[_]_; set; bag)
 open import Data.Product using (_,_)
+open import Function.Bundles using (Equivalence)
+open import Level using (Level)
 open import Relation.Unary using (Irrelevant)
 open import Relation.Binary.PropositionalEquality.Properties as ≡
 open import Relation.Binary.PropositionalEquality.WithK using (≡-irrelevant)
diff --git a/src/Data/List/Nary/NonDependent.agda b/src/Data/List/Nary/NonDependent.agda
@@ -12,8 +12,7 @@ open import Data.Nat.Base using (zero; suc)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.Product.Base as Product using (_,_)
 open import Data.Product.Nary.NonDependent using (Product)
-open import Function.Base using ()
-open import Function.Nary.NonDependent.Base
+open import Function.Nary.NonDependent.Base using (Arrows; Sets; _<$>_)
 
 ------------------------------------------------------------------------
 -- n-ary smart constructors
diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda
@@ -12,12 +12,12 @@ open import Level using (Level)
 open import Data.Bool.Base using (Bool; false; true)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.Maybe.Base using (Maybe ; nothing; just)
-open import Data.Nat.Base as ℕ
+open import Data.Nat.Base as ℕ using (ℕ; suc; zero; pred)
 open import Data.Product.Base as Prod using (∃; _×_; proj₁; proj₂; _,_; -,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
-open import Function.Base
+open import Function.Base using (id; _∘′_; _∘_; const)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl)
 open import Relation.Unary using (Pred; Decidable; U; ∅)
diff --git a/src/Data/List/NonEmpty/Effectful.agda b/src/Data/List/NonEmpty/Effectful.agda
@@ -8,14 +8,14 @@
 
 module Data.List.NonEmpty.Effectful where
 
-open import Agda.Builtin.List
+open import Agda.Builtin.List using (List; _∷_; [])
 import Data.List.Effectful as List
 open import Data.List.NonEmpty.Base
 open import Data.Product.Base using (uncurry)
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Monad
-open import Effect.Comonad
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Monad using (RawMonad)
+open import Effect.Comonad using (RawComonad)
 open import Function.Base using (flip; _∘′_; _∘_)
 
 ------------------------------------------------------------------------
diff --git a/src/Data/List/NonEmpty/Effectful/Transformer.agda b/src/Data/List/NonEmpty/Effectful/Transformer.agda
@@ -9,13 +9,13 @@
 module Data.List.NonEmpty.Effectful.Transformer where
 
 open import Data.List.NonEmpty.Base as List⁺ using (List⁺; _∷_)
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Monad
-open import Function.Base
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Monad using (RawMonad; RawMonadT)
+open import Function.Base using (_∘′_; _∘_; _$_)
 open import Level using (Level)
 
-import Data.List.NonEmpty.Effectful as List⁺
+import Data.List.NonEmpty.Effectful as List⁺ using (module TraversableM)
 
 private
   variable
diff --git a/src/Data/List/NonEmpty/Instances.agda b/src/Data/List/NonEmpty/Instances.agda
@@ -8,9 +8,10 @@
 
 module Data.List.NonEmpty.Instances where
 
-open import Data.List.NonEmpty.Effectful
-import Data.List.NonEmpty.Effectful.Transformer as Trans
-
+open import Data.List.NonEmpty.Effectful using
+  (functor; applicative; monad; comonad)
+import Data.List.NonEmpty.Effectful.Transformer as Trans using
+  (functor; applicative; monad; monadT)
 instance
   -- List⁺ instances
   nonEmptyListFunctor = functor
diff --git a/src/Data/List/NonEmpty/Relation/Unary/All.agda b/src/Data/List/NonEmpty/Relation/Unary/All.agda
@@ -8,11 +8,11 @@
 
 module Data.List.NonEmpty.Relation.Unary.All where
 
-import Data.List.Relation.Unary.All as List
+import Data.List.Relation.Unary.All as List using ([]; _∷_)
 open import Data.List.Relation.Unary.All using ([]; _∷_)
 open import Data.List.Base using ([]; _∷_)
 open import Data.List.NonEmpty.Base using (List⁺; _∷_; toList)
-open import Level
+open import Level using (Level; _⊔_)
 open import Relation.Unary using (Pred)
 
 private
diff --git a/src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda
@@ -8,13 +8,14 @@
 
 module Data.List.Relation.Binary.Disjoint.Propositional.Properties where
 
+open import Agda.Builtin.List using (List; []; _∷_)
 open import Level using (Level)
 open import Function.Base using (_∘_)
 open import Function.Bundles using (_⇔_)
-open import Data.List.Base
-open import Data.List.Relation.Binary.Disjoint.Propositional
-import Data.List.Relation.Unary.Any as Any
-open import Data.List.Relation.Unary.All as All
+open import Data.List.Base using (concat; deduplicate)
+open import Data.List.Relation.Binary.Disjoint.Propositional using (Disjoint)
+import Data.List.Relation.Unary.Any as Any using (Any)
+open import Data.List.Relation.Unary.All as All using (All)
 open import Data.List.Relation.Unary.All.Properties using (¬Any⇒All¬)
 open import Data.List.Relation.Unary.Any.Properties using (++⁻)
 open import Data.List.Membership.Propositional using (_∈_)
diff --git a/src/Data/List/Relation/Binary/Disjoint/Setoid.agda b/src/Data/List/Relation/Binary/Disjoint/Setoid.agda
@@ -6,7 +6,6 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
 
 module Data.List.Relation.Binary.Disjoint.Setoid {c ℓ} (S : Setoid c ℓ) where
@@ -17,6 +16,7 @@ open import Function.Base using (_∘_)
 open import Data.List.Base using (List; []; [_]; _∷_)
 open import Data.List.Relation.Unary.Any using (here; there)
 open import Data.Product.Base using (_×_; _,_)
+open import Relation.Binary.Core using (Rel)
 
 open Setoid S renaming (Carrier to A)
 open import Data.List.Membership.Setoid S using (_∈_; _∉_)
diff --git a/src/Data/List/Relation/Binary/Equality/Propositional.agda b/src/Data/List/Relation/Binary/Equality/Propositional.agda
@@ -15,9 +15,10 @@ open import Relation.Binary.Core using (_⇒_)
 module Data.List.Relation.Binary.Equality.Propositional {a} {A : Set a} where
 
 open import Data.List.Base
-import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
+import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality using 
+    ([]; _≋_; ≋-refl; _∷_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
-import Relation.Binary.PropositionalEquality.Properties as ≡
+import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid)
 
 ------------------------------------------------------------------------
 -- Re-export everything from setoid equality
diff --git a/src/Data/List/Relation/Binary/Equality/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Equality/Setoid/Properties.agda
@@ -15,7 +15,7 @@ module Data.List.Relation.Binary.Equality.Setoid.Properties
 open import Algebra.Bundles using (Magma; Semigroup; Monoid)
 import Algebra.Structures as Structures
 open import Data.List.Base using (List; []; _++_)
-import Data.List.Properties as List
+import Data.List.Properties as List using (++-assoc; ++-identityʳ)
 import Data.List.Relation.Binary.Equality.Setoid as ≋
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘_)
diff --git a/src/Data/List/Relation/Binary/Infix/Heterogeneous.agda b/src/Data/List/Relation/Binary/Infix/Heterogeneous.agda
@@ -8,13 +8,13 @@
 
 module Data.List.Relation.Binary.Infix.Heterogeneous where
 
-open import Level
+open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (REL; _⇒_)
 open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Data.List.Relation.Binary.Pointwise
   using (Pointwise)
-open import Data.List.Relation.Binary.Prefix.Heterogeneous
-  as Prefix using (Prefix; []; _∷_; _++ᵖ_)
+open import Data.List.Relation.Binary.Prefix.Heterogeneous as Prefix
+  using (Prefix; []; _∷_; _++ᵖ_)
 
 private
   variable
diff --git a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
@@ -16,20 +16,20 @@ open import Data.Nat.Base using (zero; suc; _≤_)
 import Data.Nat.Properties as ℕ
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (case_of_; _$′_)
-
 open import Relation.Nullary.Decidable using (yes; no; does; map′; _⊎-dec_)
 open import Relation.Nullary.Negation using (¬_; contradiction)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary.Core using (REL; _⇒_)
 open import Relation.Binary.Definitions using (Decidable; Trans; Antisym)
 open import Relation.Binary.PropositionalEquality.Core using (_≢_; refl; cong)
-open import Data.List.Relation.Binary.Pointwise.Base as Pointwise using (Pointwise)
+open import Data.List.Relation.Binary.Pointwise.Base as Pointwise
+  using (Pointwise)
 open import Data.List.Relation.Binary.Infix.Heterogeneous
-open import Data.List.Relation.Binary.Prefix.Heterogeneous
-  as Prefix using (Prefix; []; _∷_)
+open import Data.List.Relation.Binary.Prefix.Heterogeneous as Prefix
+  using (Prefix; []; _∷_)
 import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties as Prefix
-open import Data.List.Relation.Binary.Suffix.Heterogeneous
-  as Suffix using (Suffix; here; there)
+open import Data.List.Relation.Binary.Suffix.Heterogeneous as Suffix
+  using (Suffix; here; there)
 
 private
   variable
diff --git a/src/Data/List/Relation/Binary/Infix/Homogeneous/Properties.agda b/src/Data/List/Relation/Binary/Infix/Homogeneous/Properties.agda
@@ -8,16 +8,16 @@
 
 module Data.List.Relation.Binary.Infix.Homogeneous.Properties where
 
-open import Level
+open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise)
+open import Data.List.Relation.Binary.Infix.Heterogeneous using (Infix)
+open import Data.List.Relation.Binary.Infix.Heterogeneous.Properties
+  using (fromPointwise; infix?; trans; antisym)
 open import Function.Base using (_∘′_)
+open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (REL)
-open import Relation.Binary.Structures
+open import Relation.Binary.Structures 
   using (IsPreorder; IsPartialOrder; IsDecPartialOrder)
 
-open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise)
-open import Data.List.Relation.Binary.Infix.Heterogeneous
-open import Data.List.Relation.Binary.Infix.Heterogeneous.Properties
-
 private
   variable
     a b r s : Level
diff --git a/src/Data/List/Relation/Binary/Lex/NonStrict.agda b/src/Data/List/Relation/Binary/Lex/NonStrict.agda
@@ -12,20 +12,24 @@
 module Data.List.Relation.Binary.Lex.NonStrict where
 
 open import Data.Empty using (⊥)
-open import Function.Base
+open import Function.Base using (const; id)
 open import Data.Unit.Base using (⊤; tt)
-open import Data.List.Base
+open import Data.List.Base using (List; []; _∷_)
 open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; [])
 import Data.List.Relation.Binary.Lex.Strict as Strict
-open import Level
-open import Relation.Nullary
+open import Level using (Level; _⊔_)
+open import Relation.Nullary.Negation using (¬_)
+open import Relation.Nullary using (yes; no)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles
-  using (Poset; StrictPartialOrder; DecTotalOrder; StrictTotalOrder; Preorder)
+  using (Poset; StrictPartialOrder; DecTotalOrder; StrictTotalOrder;
+  Preorder)
 open import Relation.Binary.Structures
-  using (IsEquivalence; IsPartialOrder; IsStrictPartialOrder; IsTotalOrder; IsStrictTotalOrder; IsPreorder; IsDecTotalOrder)
+  using (IsEquivalence; IsPartialOrder; IsStrictPartialOrder; IsTotalOrder;
+  IsStrictTotalOrder; IsPreorder; IsDecTotalOrder)
 open import Relation.Binary.Definitions
-  using (Irreflexive; _Respects₂_; Antisymmetric; Asymmetric; Symmetric; Transitive; Decidable; Total; Trichotomous)
+  using (Irreflexive; _Respects₂_; Antisymmetric; Asymmetric; Symmetric;
+  Transitive; Decidable; Total; Trichotomous)
 import Relation.Binary.Construct.NonStrictToStrict as Conv
 
 import Data.List.Relation.Binary.Lex as Core
