[import] ... (agda#2638)

Author: jmougeot

src/Data/DifferenceList.agda

@@ -11,7 +11,7 @@ module Data.DifferenceList where
 open import Level using (Level)
 open import Data.List.Base as List using (List)
 open import Function.Base using (_⟨_⟩_)
-open import Data.Nat.Base
+open import Data.Nat.Base using (ℕ)
 
 private
   variable

src/Data/DifferenceVec.agda

@@ -8,10 +8,10 @@
 
 module Data.DifferenceVec where
 
-open import Data.DifferenceNat
+open import Data.DifferenceNat using (Diffℕ; 0#; 1#; _+_; toℕ; fromℕ; suc)
 open import Data.Vec.Base as Vec using (Vec)
 open import Function.Base using (_⟨_⟩_)
-import Data.Nat.Base as ℕ
+import Data.Nat.Base as ℕ using (ℕ; suc; _+_; zero)
 
 infixr 5 _∷_ _++_
 

src/Data/Digit.agda

@@ -11,8 +11,8 @@ module Data.Digit where
 open import Data.Nat.Base
   using (ℕ; zero; suc; _<_; _/_; _%_; sz<ss; _+_; _*_; 2+; _≤′_)
 open import Data.Nat.Properties
-  using (_≤?_; _<?_; ≤⇒≤′; module ≤-Reasoning; m≤m+n; +-comm; +-assoc;
-    *-distribˡ-+; *-identityʳ)
+  using (_≤?_; _<?_; ≤⇒≤′; module ≤-Reasoning; m≤m+n; +-comm; +-assoc
+        ; *-distribˡ-+; *-identityʳ)
 open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ)
 open import Data.Bool.Base using (Bool; true; false)
 open import Data.Char.Base using (Char)

src/Data/Vec/Effectful.agda

@@ -16,7 +16,7 @@ open import Effect.Applicative as App using (RawApplicative)
 open import Effect.Functor as Fun using (RawFunctor)
 open import Effect.Monad using (RawMonad; module Join; RawMonadT; mkRawMonad)
 import Function.Identity.Effectful as Id
-open import Function.Base
+open import Function.Base using (flip; _∘_)
 open import Level using (Level)
 
 private

src/Data/Vec/Instances.agda

@@ -8,16 +8,14 @@
 
 module Data.Vec.Instances where
 
-open import Data.Vec.Base
-open import Data.Vec.Effectful
-open import Data.Vec.Properties
-  using (≡-dec)
-open import Level
-open import Relation.Binary.PropositionalEquality.Core
+open import Data.Vec.Base using (Vec)
+open import Data.Vec.Effectful using (functor; applicative)
+open import Data.Vec.Properties using (≡-dec)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
-open import Data.Vec.Relation.Binary.Equality.DecPropositional
-open import Relation.Binary.TypeClasses
+open import Relation.Binary.TypeClasses using (IsDecEquivalence; _≟_)
 
 private
   variable

src/Data/Vec/Properties.agda

@@ -14,10 +14,11 @@ open import Data.Fin.Base as Fin
   using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_)
 open import Data.List.Base as List using (List)
 import Data.List.Properties as List
-open import Data.Nat.Base using (ℕ; zero; suc; _+_; _≤_; _<_; s≤s; pred; s<s⁻¹; _≥_;
-  s≤s⁻¹; z≤n)
+open import Data.Nat.Base
+  using (ℕ; zero; suc; _+_; _≤_; _<_; s≤s; pred; s<s⁻¹; _≥_; s≤s⁻¹; z≤n)
 open import Data.Nat.Properties
-  using (+-assoc; m≤n⇒m≤1+n; m≤m+n; ≤-refl; ≤-trans; ≤-irrelevant; ≤⇒≤″; suc-injective; +-comm; +-suc; +-identityʳ)
+  using (+-assoc; m≤n⇒m≤1+n; m≤m+n; ≤-refl; ≤-trans; ≤-irrelevant; ≤⇒≤″
+        ; suc-injective; +-comm; +-suc; +-identityʳ)
 open import Data.Product.Base as Product
   using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry)
 open import Data.Sum.Base using ([_,_]′)
@@ -34,7 +35,8 @@ open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary.Decidable.Core using (Dec; does; yes; _×-dec_; map′)
+open import Relation.Nullary.Decidable.Core
+  using (Dec; does; yes; _×-dec_; map′)
 open import Relation.Nullary.Negation.Core using (contradiction)
 import Data.Nat.GeneralisedArithmetic as ℕ
 

src/Data/Vec/Recursive.agda

@@ -18,7 +18,7 @@ module Data.Vec.Recursive where
 
 open import Data.Nat.Base as Nat using (ℕ; zero; suc; NonZero; pred)
 open import Data.Nat.Properties using (+-comm; *-comm)
-open import Data.Empty.Polymorphic
+open import Data.Empty.Polymorphic using (⊥)
 open import Data.Fin.Base as Fin using (Fin; zero; suc)
 open import Data.Fin.Properties using (1↔⊤; *↔×)
 open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)

src/Data/Vec/Reflection.agda

@@ -8,10 +8,10 @@
 
 module Data.Vec.Reflection where
 
-import Data.List.Base as List
-open import Data.Vec.Base
-open import Reflection.AST.Term
-open import Reflection.AST.Argument
+import Data.List.Base as List using (List; [])
+open import Data.Vec.Base as Vec using (Vec; _∷_; [])
+open import Reflection.AST.Term using (Term; def; con; _⋯⟅∷⟆_)
+open import Reflection.AST.Argument using (_⟨∷⟩_)
 
 ------------------------------------------------------------------------
 -- Type

src/Data/Vec/Show.agda

@@ -8,7 +8,7 @@
 
 module Data.Vec.Show where
 
-import Data.List.Show as List
+import Data.List.Show as List using (show)
 open import Data.String.Base using (String)
 open import Data.Vec.Base using (Vec; toList)
 open import Function.Base using (_∘_)

src/Data/W/Indexed.agda

@@ -8,10 +8,10 @@
 
 module Data.W.Indexed where
 
-open import Level
-open import Data.Container.Indexed.Core
+open import Level using (Level; _⊔_)
+open import Data.Container.Indexed.Core using (Container; ⟦_⟧; □)
 open import Data.Product.Base using (_,_; Σ)
-open import Relation.Unary
+open import Relation.Unary using (Pred; _⊆_; _∩_; _∪_)
 
 -- The family of indexed W-types.