[Import] (#2639)

Author: jmougeot

src/Debug/Trace.agda

@@ -10,8 +10,8 @@
 
 module Debug.Trace where
 
-open import Agda.Builtin.String
-open import Agda.Builtin.Equality
+open import Agda.Builtin.String using (String)
+open import Agda.Builtin.Equality using (_≡_)
 
 -- Postulating the `trace` function and explaining how to compile it
 

src/Effect/Applicative.agda

@@ -14,11 +14,9 @@ module Effect.Applicative where
 open import Data.Bool.Base using (Bool; true; false)
 open import Data.Product.Base using (_×_; _,_)
 open import Data.Unit.Polymorphic.Base using (⊤)
-
 open import Effect.Choice using (RawChoice)
 open import Effect.Empty using (RawEmpty)
 open import Effect.Functor as Fun using (RawFunctor)
-
 open import Function.Base using (const; flip; _∘′_)
 open import Level using (Level; suc; _⊔_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)

src/Effect/Applicative/Indexed.agda

@@ -13,8 +13,8 @@ module Effect.Applicative.Indexed where
 
 open import Effect.Functor using (RawFunctor)
 open import Data.Product.Base using (_×_; _,_)
-open import Function.Base
-open import Level
+open import Function.Base using (const; constᵣ)
+open import Level using (Level; suc; _⊔_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)

src/Effect/Applicative/Predicate.agda

@@ -14,8 +14,8 @@ module Effect.Applicative.Predicate where
 open import Effect.Functor.Predicate
 open import Data.Product.Base using (_,_)
 open import Function.Base using (const; constᵣ)
-open import Level
-open import Relation.Unary
+open import Level using (Level; suc; _⊔_)
+open import Relation.Unary using (_⊆_; _⇒_; _∩_)
 open import Relation.Unary.PredicateTransformer using (Pt)
 
 private

src/Effect/Comonad.agda

@@ -10,7 +10,7 @@
 
 module Effect.Comonad where
 
-open import Level
+open import Level using (Level; suc)
 open import Function.Base using (id; _∘′_; flip)
 
 private

src/Effect/Empty.agda

@@ -8,7 +8,7 @@
 
 module Effect.Empty where
 
-open import Level
+open import Level using (Level; suc; _⊔_)
 
 private
   variable

src/Effect/Foldable.agda

@@ -13,11 +13,8 @@ module Effect.Foldable where
 open import Algebra.Bundles.Raw using (RawMonoid)
 open import Algebra.Bundles using (Monoid)
 import Algebra.Construct.Flip.Op as Op
-
 open import Data.List.Base as List using (List; [_]; _++_)
-
 open import Effect.Functor as Fun using (RawFunctor)
-
 open import Function.Base using (id; flip)
 open import Function.Endo.Propositional using (∘-id-monoid)
 open import Level using (Level; Setω)

src/Effect/Functor.agda

@@ -12,8 +12,7 @@ module Effect.Functor where
 
 open import Data.Unit.Polymorphic.Base using (⊤)
 open import Function.Base using (const; flip)
-open import Level
-
+open import Level using (Level; suc; _⊔_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 private

src/Effect/Functor/Predicate.agda

@@ -11,8 +11,8 @@
 module Effect.Functor.Predicate where
 
 open import Function.Base using (const)
-open import Level
-open import Relation.Unary
+open import Level using (Level; suc; _⊔_)
+open import Relation.Unary using (_⊆_)
 open import Relation.Unary.PredicateTransformer using (PT)
 
 private

src/Effect/Monad.agda

@@ -12,10 +12,10 @@ module Effect.Monad where
 
 open import Data.Bool.Base using (Bool; true; false; not)
 open import Data.Unit.Polymorphic.Base using (⊤)
-
-open import Effect.Choice
-open import Effect.Empty
-open import Effect.Applicative
+open import Effect.Choice using (RawChoice)
+open import Effect.Empty using (RawEmpty)
+open import Effect.Applicative as App
+  using (RawApplicative; RawApplicativeZero; mkRawApplicative; RawAlternative)
 open import Function.Base using (id; flip; _$′_; _∘′_)
 open import Level using (Level; suc; _⊔_)