[import] ... (#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.
 

src/Data/W/Sized.agda

@@ -8,8 +8,8 @@
 
 module Data.W.Sized where
 
-open import Level
-open import Size
+open import Level using (Level; _⊔_)
+open import Size using (Size; ↑_; ∞)
 open import Function.Base using (_$_; _∘_; const)
 open import Data.Product.Base using (_,_; -,_; proj₂)
 open import Data.Container.Core as Container using (Container; ⟦_⟧; Shape; Position; _⇒_; ⟪_⟫)

src/Data/W/WithK.agda

@@ -9,9 +9,9 @@
 module Data.W.WithK where
 
 open import Data.Product.Base using (_,_)
-open import Data.Container.Core
-open import Data.W
-open import Agda.Builtin.Equality
+open import Data.Container.Core using (Container; Shape; Position; _⇒_)
+open import Data.W using (W; sup)
+open import Agda.Builtin.Equality using (_≡_; refl)
 
 module _ {s p} {C : Container s p}
          {s : Shape C} {f : Position C s → W C} where

src/Data/Word64/Instances.agda

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

src/Data/Word64/Properties.agda

@@ -17,7 +17,7 @@ open import Relation.Binary
   using ( _⇒_; Reflexive; Symmetric; Transitive; Substitutive
         ; Decidable; DecidableEquality; IsEquivalence; IsDecEquivalence
         ; Setoid; DecSetoid; StrictTotalOrder)
-import Relation.Binary.Construct.On as On
+import Relation.Binary.Construct.On as On using (decidable; strictTotalOrder)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; cong; sym; trans; subst)
 open import Relation.Binary.PropositionalEquality.Properties

src/Data/Word64/Show.agda

@@ -12,13 +12,11 @@ open import Agda.Builtin.String using (String)
 
 open import Data.Bool.Show using (showBit)
 open import Data.Fin.Base as Fin using (Fin)
-import Data.Nat.Show as ℕ
+import Data.Nat.Show as ℕ using (showInBase)
 open import Data.String using (_++_; fromVec; padLeft)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
-
-open import Data.Word64.Base
-open import Data.Word64.Unsafe
-
+open import Data.Word64.Base using (Word64; toℕ)
+open import Data.Word64.Unsafe using (toBits)
 open import Function.Base using (_$_)
 
 showBits : Word64 → String

src/Data/Word64/Unsafe.agda

@@ -13,7 +13,7 @@ open import Data.Fin.Base as Fin using (Fin)
 open import Data.Product.Base using (proj₁)
 open import Data.Vec.Base as Vec using (Vec)
 open import Data.Word8.Base as Word8 using (Word8)
-open import Data.Word64.Base
+open import Data.Word64.Base using (Word64; fromℕ)
 open import Function.Base using (_$_; _|>_)
 
 ------------------------------------------------------------------------

src/Data/Word8/Base.agda

@@ -12,10 +12,8 @@ open import Agda.Builtin.Bool using (Bool; true; false)
 open import Agda.Builtin.Char using (Char)
 open import Agda.Builtin.Nat using (Nat; _==_)
 open import Agda.Builtin.Unit using (⊤)
-
 open import Data.Fin.Base as Fin using (Fin)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
-
 open import Function.Base using (_$_; _|>_)
 
 ------------------------------------------------------------------------------

src/Data/Word8/Show.agda

@@ -12,10 +12,10 @@ open import Agda.Builtin.String using (String)
 
 open import Data.Bool.Show using (showBit)
 open import Data.Fin.Base as Fin using (Fin)
-import Data.Nat.Show as ℕ
+import Data.Nat.Show as ℕ using (showInBase)
 open import Data.String using (_++_; fromVec; padLeft)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
-open import Data.Word8.Base
+open import Data.Word8.Base using (Word8; toℕ; toBits)
 open import Function.Base using (_$_)
 
 showBits : Word8 → String