[Import] Data.List.* (#2625)

* [Import] Data.List

* fix

* fix

* fix

* fix

* fix

* fix

* fix

* Update src/Data/List/NonEmpty/Effectful.agda

Resolves question about use of `Agda.Builtin` here.
Originally it solved a dependency/ambiguity conflict, but the generally strategy of localising imports pays off in this case!

* Update src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda

Reorder to reflect conventions on dependency.

---------

Co-authored-by: jamesmckinna <[email protected]>

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
 

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; _∘_)

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)

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

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; ∅)

src/Data/List/NonEmpty/Effectful.agda

@@ -8,14 +8,14 @@
 
 module Data.List.NonEmpty.Effectful where
 
-open import Agda.Builtin.List
+open import Data.List.Base 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; _∘′_; _∘_)
 
 ------------------------------------------------------------------------

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

src/Data/List/NonEmpty/Instances.agda

@@ -9,8 +9,9 @@
 module Data.List.NonEmpty.Instances where
 
 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

src/Data/List/NonEmpty/Relation/Unary/All.agda

@@ -12,7 +12,7 @@ import Data.List.Relation.Unary.All as List
 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

src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda

@@ -8,18 +8,19 @@
 
 module Data.List.Relation.Binary.Disjoint.Propositional.Properties where
 
-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 (List; []; _∷_; 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 (_∈_)
 open import Data.Product.Base as Product using (_,_)
 open import Data.Sum.Base using (inj₁; inj₂)
+open import Function.Base using (_∘_)
+open import Function.Bundles using (_⇔_)
+open import Level using (Level)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions using (Symmetric; DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)

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 (_∈_; _∉_)

src/Data/List/Relation/Binary/Equality/Propositional.agda

@@ -17,7 +17,7 @@ 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
 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

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 (_∘_)

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

src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda

@@ -8,28 +8,29 @@
 
 module Data.List.Relation.Binary.Infix.Heterogeneous.Properties where
 
-open import Level
+open import Level using (Level; _⊔_)
 open import Data.Bool.Base using (true; false)
 open import Data.Empty using (⊥-elim)
 open import Data.List.Base as List using (List; []; _∷_; length; map; filter; replicate)
+open import Data.List.Relation.Binary.Infix.Heterogeneous
+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.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.Nullary.Negation.Core 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.Infix.Heterogeneous
-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.Pointwise.Base as Pointwise
+  using (Pointwise)
+
 
 private
   variable

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
   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

src/Data/List/Relation/Binary/Lex/NonStrict.agda

@@ -12,20 +12,22 @@
 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.List.Base
+open import Data.List.Base using (List; []; _∷_)
 open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; [])
+open import Function.Base using (const; id)
 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.Core 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)
 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