[Import] ... (#2637)

Author: jmougeot

src/Data/Trie/NonEmpty.agda

@@ -10,17 +10,19 @@ open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Trie.NonEmpty {k e r} (S : StrictTotalOrder k e r) where
 
-open import Level
-open import Size
-open import Effect.Monad
 open import Data.Product.Base as Product using (∃; uncurry; -,_)
 open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; [_]; concatMap)
-open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′) hiding (module Maybe)
+open import Data.Maybe.Base as Maybe
+  using (Maybe; nothing; just; maybe′) hiding (module Maybe)
 open import Data.These as These using (These; this; that; these)
+open import Effect.Monad using (RawMonad)
 open import Function.Base as F
+  using (const; _∘′_; _$_; id; _∘_; _$′_; case_of_)
+open import Level using (Level; _⊔_)
 import Function.Identity.Effectful as Identity
 open import Relation.Unary using (_⇒_; IUniversal)
+open import Size using (Size; ↑_; ∞)
 
 open StrictTotalOrder S
   using (module Eq)

src/Data/Unit/Instances.agda

@@ -8,7 +8,7 @@
 
 module Data.Unit.Instances where
 
-open import Data.Unit.Properties
+open import Data.Unit.Properties using (_≟_; ≡-isDecTotalOrder)
 open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
 

src/Data/Unit/NonEta.agda

@@ -8,7 +8,7 @@
 
 module Data.Unit.NonEta where
 
-open import Level
+open import Level using (_⊔_; Level)
 
 ------------------------------------------------------------------------
 -- A unit type defined as a data-type

src/Data/Unit/Polymorphic/Base.agda

@@ -8,7 +8,7 @@
 
 module Data.Unit.Polymorphic.Base where
 
-open import Level
+open import Level using (Level; Lift; lift)
 import Data.Unit.Base as ⊤
 
 ------------------------------------------------------------------------

src/Data/Unit/Polymorphic/Instances.agda

@@ -8,9 +8,9 @@
 
 module Data.Unit.Polymorphic.Instances where
 
-open import Data.Unit.Polymorphic.Base
-open import Data.Unit.Polymorphic.Properties
-open import Level
+open import Data.Unit.Polymorphic.Base using (⊤)
+open import Data.Unit.Polymorphic.Properties using (_≟_; ≡-isDecTotalOrder)
+open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)

src/Data/Unit/Properties.agda

@@ -16,7 +16,8 @@ open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; Poset; DecTotalOrder)
 open import Relation.Binary.Structures
   using (IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder)
-open import Relation.Binary.Definitions using (DecidableEquality; Total; Antisymmetric)
+open import Relation.Binary.Definitions
+  using (DecidableEquality; Total; Antisymmetric)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; trans)
 open import Relation.Binary.PropositionalEquality.Properties
@@ -92,3 +93,4 @@ _ ≟ _ = yes refl
 ≡-decTotalOrder = record
   { isDecTotalOrder = ≡-isDecTotalOrder
   }
+

src/Data/Universe/Indexed.agda

@@ -9,9 +9,9 @@
 module Data.Universe.Indexed where
 
 open import Data.Product.Base using (∃; proj₂)
-open import Data.Universe
+open import Data.Universe using (Universe)
 open import Function.Base using (_∘_)
-open import Level
+open import Level using (Level; _⊔_; suc)
 
 ------------------------------------------------------------------------
 -- Definitions

src/Data/Vec/Bounded/Base.agda

@@ -8,10 +8,10 @@
 
 module Data.Vec.Bounded.Base where
 
-open import Data.Nat.Base
+open import Data.Nat.Base as ℕ
+  using (ℕ; suc; zero; _+_; _∸_; _⊓_; _⊔_; _≤_; ⌊_/2⌋; ⌈_/2⌉; z≤n; s≤s; s≤s⁻¹)
 import Data.Nat.Properties as ℕ
 open import Data.List.Base as List using (List)
-open import Data.List.Extrema ℕ.≤-totalOrder
 open import Data.List.Relation.Unary.All as All using (All)
 import Data.List.Relation.Unary.All.Properties as All
 open import Data.List.Membership.Propositional using (mapWith∈)
@@ -25,6 +25,8 @@ open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
 
+open import Data.List.Extrema ℕ.≤-totalOrder
+
 private
   variable
     a b c p : Level

src/Data/Vec/Bounded/Show.agda

@@ -10,7 +10,7 @@ module Data.Vec.Bounded.Show where
 
 open import Data.String.Base using (String)
 open import Data.Vec.Bounded.Base using (Vec≤)
-import Data.Vec.Show as Vec
+import Data.Vec.Show as Vec using (show)
 open import Function.Base using (_∘_)
 
 show : ∀ {a} {A : Set a} {n} → (A → String) → (Vec≤ A n → String)

src/Data/Vec/Effectful/Transformer.agda

@@ -10,11 +10,11 @@ module Data.Vec.Effectful.Transformer where
 
 open import Data.Nat.Base using (ℕ)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Monad
-open import Function.Base
-open import Level
+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.Vec.Effectful as Vec
 

src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda

@@ -17,7 +17,7 @@ open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Vec.Functional as VF hiding (map)
 open import Data.Vec.Functional.Relation.Binary.Pointwise
-open import Function.Base
+open import Function.Base using (const; _∘_)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel; REL)
 open import Relation.Binary.Bundles using (Setoid; DecSetoid)

src/Data/Vec/Functional/Relation/Unary/All.agda

@@ -12,7 +12,7 @@ open import Data.Fin.Properties using (all?)
 open import Data.Product.Base using (_,_)
 open import Data.Vec.Functional as VF hiding (map)
 open import Level using (Level)
-open import Relation.Unary
+open import Relation.Unary using (Pred; _⊆_; Decidable; Universal; Satisfiable)
 
 private
   variable

src/Data/Vec/Functional/Relation/Unary/All/Properties.agda

@@ -17,7 +17,7 @@ open import Data.Vec.Functional as VF hiding (map)
 open import Data.Vec.Functional.Relation.Unary.All
 open import Function.Base using (const; _∘_)
 open import Level using (Level)
-open import Relation.Unary
+open import Relation.Unary using (Pred; _⟨×⟩_)
 
 private
   variable

src/Data/Vec/Functional/Relation/Unary/Any.agda

@@ -10,12 +10,12 @@ module Data.Vec.Functional.Relation.Unary.Any where
 
 open import Data.Fin.Base using (zero; suc)
 open import Data.Fin.Properties using (any?)
-open import Data.Nat.Base
+open import Data.Nat.Base using (ℕ)
 open import Data.Product.Base as Σ using (Σ; ∃; _×_; _,_; proj₁; proj₂)
 open import Data.Vec.Functional as VF hiding (map)
 open import Function.Base using (id)
 open import Level using (Level)
-open import Relation.Unary
+open import Relation.Unary using (Pred; _⊆_; Decidable)
 
 private
   variable

src/Data/Vec/Properties/WithK.agda

@@ -9,7 +9,7 @@
 
 module Data.Vec.Properties.WithK where
 
-open import Data.Nat.Base
+open import Data.Nat.Base using (ℕ; suc)
 open import Data.Nat.Properties using (+-assoc)
 open import Data.Vec.Base
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)

src/Data/Vec/Recursive/Effectful.agda

@@ -8,7 +8,7 @@
 
 module Data.Vec.Recursive.Effectful where
 
-open import Agda.Builtin.Nat
+open import Agda.Builtin.Nat using (suc; zero)
 open import Data.Product.Base hiding (map)
 open import Data.Vec.Recursive
 open import Effect.Functor

src/Data/Vec/Relation/Binary/Lex/Core.agda

@@ -8,9 +8,9 @@
 
 module Data.Vec.Relation.Binary.Lex.Core {a} {A : Set a} where
 
-open import Data.Empty
+open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat.Base using (ℕ; suc)
-import Data.Nat.Properties as ℕ
+import Data.Nat.Properties as ℕ using (_≟_; ≡-irrelevant)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; uncurry)
 open import Data.Vec.Base using (Vec; []; _∷_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
@@ -20,7 +20,8 @@ open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (Rel; REL)
 open import Relation.Binary.Definitions
-  using (Transitive; Symmetric; Asymmetric; Antisymmetric; Irreflexive; Trans; _Respects₂_; _Respectsˡ_; _Respectsʳ_; Decidable; Irrelevant)
+  using (Transitive; Symmetric; Asymmetric; Antisymmetric; Irreflexive; Trans
+        ; _Respects₂_; _Respectsˡ_; _Respectsʳ_; Decidable; Irrelevant)
 open import Relation.Binary.Structures using (IsPartialEquivalence)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; refl; cong)

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

@@ -11,7 +11,7 @@
 
 module Data.Vec.Relation.Binary.Lex.NonStrict where
 
-open import Data.Empty
+open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Unit.Base using (⊤; tt)
 open import Data.Product.Base using (proj₁; proj₂)
 open import Data.Nat.Base using (ℕ)
@@ -23,11 +23,15 @@ open import Function.Base using (id)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (REL; Rel; _⇒_)
 open import Relation.Binary.Bundles
-  using (Poset; StrictPartialOrder; DecPoset; DecStrictPartialOrder; DecTotalOrder; StrictTotalOrder; Preorder; TotalOrder)
+  using (Poset; StrictPartialOrder; DecPoset; DecStrictPartialOrder
+        ; DecTotalOrder; StrictTotalOrder; Preorder; TotalOrder)
 open import Relation.Binary.Structures
-  using (IsEquivalence; IsPartialOrder; IsStrictPartialOrder; IsDecPartialOrder; IsDecStrictPartialOrder; IsDecTotalOrder; IsStrictTotalOrder; IsPreorder; IsTotalOrder)
+  using (IsEquivalence; IsPartialOrder; IsStrictPartialOrder; IsDecPartialOrder
+        ; IsDecStrictPartialOrder; IsDecTotalOrder; IsStrictTotalOrder
+        ; IsPreorder; IsTotalOrder)
 open import Relation.Binary.Definitions
-  using (Irreflexive; _Respects₂_; Antisymmetric; Asymmetric; Symmetric; Trans; Decidable; Total; Trichotomous)
+  using (Irreflexive; _Respects₂_; Antisymmetric; Asymmetric; Symmetric; Trans
+        ; Decidable; Total; Trichotomous)
 import Relation.Binary.Construct.NonStrictToStrict as Conv
 open import Relation.Nullary hiding (Irrelevant)
 

src/Data/Vec/Relation/Binary/Lex/Strict.agda

@@ -26,12 +26,17 @@ open import Induction.WellFounded
 open import Relation.Nullary using (yes; no; ¬_)
 open import Relation.Binary.Core using (REL; Rel; _⇒_)
 open import Relation.Binary.Bundles
-  using (Poset; StrictPartialOrder; DecPoset; DecStrictPartialOrder; DecTotalOrder; StrictTotalOrder; Preorder; TotalOrder)
+  using (Poset; StrictPartialOrder; DecPoset; DecStrictPartialOrder
+        ; DecTotalOrder; StrictTotalOrder; Preorder; TotalOrder)
 open import Relation.Binary.Structures
-  using (IsEquivalence; IsPartialOrder; IsStrictPartialOrder; IsDecPartialOrder; IsDecStrictPartialOrder; IsDecTotalOrder; IsStrictTotalOrder; IsPreorder; IsTotalOrder; IsPartialEquivalence)
+  using (IsEquivalence; IsPartialOrder; IsStrictPartialOrder; IsDecPartialOrder
+        ; IsDecStrictPartialOrder; IsDecTotalOrder; IsStrictTotalOrder
+        ; IsPreorder; IsTotalOrder; IsPartialEquivalence)
 open import Relation.Binary.Definitions
-  using (Irreflexive; _Respects₂_; _Respectsˡ_; _Respectsʳ_; Antisymmetric; Asymmetric; Symmetric; Trans; Decidable; Total; Trichotomous; Transitive; Irrelevant; tri≈; tri>; tri<)
-open import Relation.Binary.Consequences
+  using (Irreflexive; _Respects₂_; _Respectsˡ_; _Respectsʳ_; Antisymmetric
+        ; Asymmetric; Symmetric; Trans; Decidable; Total; Trichotomous
+        ; Transitive; Irrelevant; tri≈; tri>; tri<)
+open import Relation.Binary.Consequences using (asym⇒irr)
 open import Relation.Binary.Construct.On as On using (wellFounded)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Level using (Level; _⊔_)

src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda

@@ -25,7 +25,7 @@ open import Relation.Binary.Definitions using (Reflexive; Sym; Trans; Decidable)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Binary.Construct.Closure.Transitive as Plus
   hiding (equivalent; map)
-open import Relation.Nullary
+open import Relation.Nullary.Negation.Core using (¬_)
 import Relation.Nullary.Decidable as Dec
 
 private