[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; _⊔_)
 

src/Effect/Monad/Indexed.agda

@@ -11,8 +11,9 @@
 module Effect.Monad.Indexed where
 
 open import Effect.Applicative.Indexed
-open import Function.Base
-open import Level
+  using (IFun; RawIApplicative; RawIApplicativeZero; RawIAlternative)
+open import Function.Base using (id; _∘_)
+open import Level using (Level; _⊔_; suc)
 
 private
   variable

src/Effect/Monad/Partiality/All.agda

@@ -8,11 +8,11 @@
 
 module Effect.Monad.Partiality.All where
 
-open import Effect.Monad
+open import Effect.Monad using (RawMonad)
 open import Effect.Monad.Partiality as Partiality using (_⊥; ⇒≈)
-open import Codata.Musical.Notation
+open import Codata.Musical.Notation using (♭; ∞; ♯_)
 open import Function.Base using (flip; _∘_)
-open import Level
+open import Level using (Level; _⊔_; suc)
 open import Relation.Binary.Definitions using (_Respects_)
 open import Relation.Binary.Structures using (IsEquivalence)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)

src/Effect/Monad/Reader/Indexed.agda

@@ -14,8 +14,8 @@ open import Function.Base using (const; flip; _∘_)
 open import Function.Identity.Effectful as Id using (Identity)
 open import Effect.Applicative.Indexed
   using (IFun; RawIApplicative; RawIApplicativeZero; RawIAlternative)
-open import Effect.Monad.Indexed using (RawIMonad; RawIMonadZero;
-  RawIMonadPlus)
+open import Effect.Monad.Indexed
+  using (RawIMonad; RawIMonadZero; RawIMonadPlus)
 
 private
   variable

src/Effect/Monad/State/Indexed.agda

@@ -12,8 +12,8 @@ open import Effect.Applicative.Indexed
   using (IFun; RawIApplicative; RawIApplicativeZero; RawIAlternative)
 open import Effect.Monad using (RawMonad; RawMonadZero; RawMonadPlus)
 open import Function.Identity.Effectful as Id using (Identity)
-open import Effect.Monad.Indexed using (RawIMonad; RawIMonadZero;
-  RawIMonadPlus)
+open import Effect.Monad.Indexed
+  using (RawIMonad; RawIMonadZero; RawIMonadPlus)
 open import Data.Product.Base using (_×_; _,_; uncurry)
 open import Data.Unit.Polymorphic using (⊤)
 open import Function.Base using (const; _∘_)

src/Effect/Monad/State/Transformer/Base.agda

@@ -11,11 +11,10 @@ module Effect.Monad.State.Transformer.Base where
 
 open import Data.Product.Base using (_×_; proj₁; proj₂)
 open import Data.Unit.Polymorphic.Base using (⊤)
+open import Effect.Functor using (RawFunctor)
 open import Function.Base using (_∘′_; const; id)
 open import Level using (Level; suc; _⊔_)
 
-open import Effect.Functor
-
 private
   variable
     f s : Level

src/Effect/Monad/Writer/Indexed.agda

@@ -12,10 +12,11 @@ module Effect.Monad.Writer.Indexed (a : Level) where
 
 open import Algebra using (RawMonoid)
 open import Data.Product.Base using (_×_; _,_; map₁)
-open import Data.Unit.Polymorphic
+open import Data.Unit.Polymorphic using (⊤; tt)
 open import Effect.Applicative.Indexed
-open import Effect.Monad
+  using (IFun; RawIApplicative; RawIApplicativeZero; RawIAlternative)
 open import Effect.Monad.Indexed
+  using (RawIMonad; RawIMonadZero; RawIMonadPlus)
 open import Function.Base using (_∘′_)
 open import Function.Identity.Effectful as Id using (Identity)
 

src/Effect/Monad/Writer/Transformer/Base.agda

@@ -11,11 +11,10 @@ module Effect.Monad.Writer.Transformer.Base where
 open import Algebra using (RawMonoid)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Data.Unit.Polymorphic using (⊤; tt)
+open import Effect.Functor using (RawFunctor)
 open import Function.Base using (id; _∘′_)
 open import Level using (Level; suc; _⊔_)
 
-open import Effect.Functor using (RawFunctor)
-
 private
   variable
     w f g : Level