Skip to content

[ cleanup ] imports in the Effect.Monad modules #2371

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
MatthewDaggitt merged 1 commit into from
Apr 21, 2024
Merged

[ cleanup ] imports in the Effect.Monad modules #2371

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 4 additions & 5 deletions src/Effect/Monad/Continuation.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,12 @@

module Effect.Monad.Continuation where

open import Effect.Applicative
open import Effect.Applicative.Indexed
open import Effect.Monad
open import Effect.Applicative.Indexed using (IFun)
open import Effect.Monad using (RawMonad)
open import Function.Identity.Effectful as Id using (Identity)
open import Effect.Monad.Indexed
open import Effect.Monad.Indexed using (RawIMonad)
open import Function.Base using (flip)
open import Level
open import Level using (Level; _⊔_; suc)

private
variable
Expand Down
10 changes: 3 additions & 7 deletions src/Effect/Monad/Error/Transformer.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,16 +6,12 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Level
open import Level using (Level; _⊔_; suc)

module Effect.Monad.Error.Transformer {e} (E : Set e) (a : Level) where

open import Effect.Choice
open import Effect.Empty
open import Effect.Functor
open import Effect.Applicative
open import Effect.Monad
open import Function.Base
open import Effect.Monad using (RawMonad)
open import Function.Base using (_∘′_; _$_)

private
variable
Expand Down
8 changes: 3 additions & 5 deletions src/Effect/Monad/IO.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,15 +6,13 @@

{-# OPTIONS --cubical-compatible --guardedness #-}

open import Level

module Effect.Monad.IO where

open import Data.Product.Base using (_,_)
open import Function.Base
open import Effect.Functor using (RawFunctor)
open import Function.Base using (id)
open import IO.Base using (IO)
open import Effect.Functor
open import Effect.Monad
open import Level using (Level; suc)

private
variable
Expand Down
10 changes: 5 additions & 5 deletions src/Effect/Monad/Identity.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,12 +8,12 @@

module Effect.Monad.Identity where

open import Effect.Functor
open import Effect.Applicative
open import Effect.Monad
open import Effect.Comonad
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative using (RawApplicative)
open import Effect.Monad using (RawMonad; module Join)
open import Effect.Comonad using (RawComonad)
open import Function.Base using (id; _∘′_; _|>′_; _$′_; flip)
open import Level
open import Level using (Level)

private
variable
Expand Down
6 changes: 3 additions & 3 deletions src/Effect/Monad/Partiality.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,13 +9,13 @@
module Effect.Monad.Partiality where

open import Codata.Musical.Notation using (∞; ♯_; ♭)
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative using (RawApplicative)
open import Effect.Monad using (RawMonad; module Join)
open import Data.Bool.Base using (Bool; false; true)
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Data.Product as Prod using (∃; ∄; -,_; ∃₂; _,_; _×_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative using (RawApplicative)
open import Effect.Monad using (RawMonad; module Join)
open import Function.Base using (_∘′_; flip; id; _∘_; _$_; _⟨_⟩_)
open import Function.Bundles using (_⇔_; mk⇔)
open import Level using (Level; _⊔_)
Expand Down
6 changes: 3 additions & 3 deletions src/Effect/Monad/Predicate.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,10 @@

module Effect.Monad.Predicate where

open import Effect.Monad.Indexed using (RawIMonad)
open import Data.Product.Base using (_,_)
open import Effect.Monad.Indexed using (RawIMonad)
open import Function.Base using (const; id; _∘_)
open import Level using (Level; suc; _⊔_)
open import Level using (Level; _⊔_; suc)
open import Relation.Binary.PropositionalEquality.Core using (refl)
open import Relation.Unary using (_⊆_; _⇒_; _∈_; _∩_; ｛_｝)
open import Relation.Unary.PredicateTransformer using (Pt)
Expand All @@ -24,7 +24,7 @@ private

------------------------------------------------------------------------

record RawPMonad {I : Set i} (M : Pt I (i ⊔ ℓ)) : Set (suc i ⊔ suc ℓ) where
record RawPMonad {I : Set i} (M : Pt I (i ⊔ ℓ)) : Set (suc (i ⊔ ℓ)) where

infixl 1 _?>=_ _?>_ _>?>_ _?>=′_
infixr 1 _=<?_ _<?<_
Expand Down
10 changes: 3 additions & 7 deletions src/Effect/Monad/Reader.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,15 +6,11 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Level

module Effect.Monad.Reader where

open import Effect.Choice
open import Effect.Empty
open import Effect.Functor
open import Effect.Applicative
open import Effect.Monad
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative using (RawApplicative)
open import Effect.Monad using (RawMonad; module Join)
open import Effect.Monad.Identity as Id using (Identity; runIdentity)
open import Level using (Level)

Expand Down
10 changes: 5 additions & 5 deletions src/Effect/Monad/Reader/Transformer.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,11 @@
module Effect.Monad.Reader.Transformer where

open import Algebra using (RawMonoid)
open import Effect.Choice
open import Effect.Empty
open import Effect.Functor
open import Effect.Applicative
open import Effect.Monad
open import Effect.Choice using (RawChoice)
open import Effect.Empty using (RawEmpty)
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative using (RawApplicative; RawApplicativeZero; RawAlternative)
open import Effect.Monad using (RawMonad; RawMonadZero; RawMonadPlus; RawMonadT)
open import Function.Base using (_∘′_; const; _$_)
open import Level using (Level; _⊔_)

Expand Down
12 changes: 4 additions & 8 deletions src/Effect/Monad/State.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,18 +6,14 @@

{-# OPTIONS --cubical-compatible --safe #-}


module Effect.Monad.State where

open import Data.Product.Base using (_×_)
open import Effect.Choice
open import Effect.Empty
open import Effect.Functor
open import Effect.Applicative
open import Effect.Monad
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative using (RawApplicative)
open import Effect.Monad using (RawMonad; module Join)
open import Effect.Monad.Identity as Id using (Identity; runIdentity)
open import Function.Base
open import Level
open import Level using (Level)

import Effect.Monad.State.Transformer as Trans

Expand Down
19 changes: 9 additions & 10 deletions src/Effect/Monad/State/Transformer.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,21 +6,20 @@

{-# OPTIONS --cubical-compatible --safe #-}

open import Level using (Level; suc; _⊔_)

module Effect.Monad.State.Transformer where

open import Algebra using (RawMonoid)
open import Data.Product.Base using (_×_; _,_; map₂; proj₁; proj₂)
open import Data.Unit.Polymorphic.Base
open import Effect.Choice
open import Effect.Empty
open import Effect.Functor
open import Effect.Applicative
open import Effect.Monad
open import Function.Base

open import Effect.Monad.Reader.Transformer using (RawMonadReader)
open import Data.Unit.Polymorphic.Base using (tt)
open import Effect.Choice using (RawChoice)
open import Effect.Empty using (RawEmpty)
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative using (RawApplicative; RawApplicativeZero; RawAlternative)
open import Effect.Monad using (RawMonad; RawMonadZero; RawMonadPlus; RawMonadT; RawMonadTd)
open import Function.Base using (_∘′_; _$_; const)
open import Level using (Level; _⊔_)


private
variable
Expand Down
9 changes: 3 additions & 6 deletions src/Effect/Monad/Writer.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,13 +10,10 @@ module Effect.Monad.Writer where

open import Algebra using (RawMonoid)
open import Data.Product.Base using (_×_)
open import Effect.Applicative
open import Effect.Choice
open import Effect.Empty
open import Effect.Functor
open import Effect.Monad
open import Effect.Applicative using (RawApplicative)
open import Effect.Functor using (RawFunctor)
open import Effect.Monad using (RawMonad; module Join)
open import Effect.Monad.Identity as Id using (Identity; runIdentity)
open import Function.Base using (_∘′_)
open import Level using (Level)

import Effect.Monad.Writer.Transformer as Trans
Expand Down
12 changes: 6 additions & 6 deletions src/Effect/Monad/Writer/Transformer.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,13 +11,13 @@ module Effect.Monad.Writer.Transformer where

open import Algebra using (RawMonoid)
open import Data.Product.Base using (_×_; _,_; proj₂; map₂)
open import Effect.Applicative
open import Effect.Choice
open import Effect.Empty
open import Effect.Functor
open import Effect.Monad
open import Effect.Applicative using (RawApplicative; RawApplicativeZero; RawAlternative)
open import Effect.Choice using (RawChoice)
open import Effect.Empty using (RawEmpty)
open import Effect.Functor using (RawFunctor)
open import Effect.Monad using (RawMonad; RawMonadZero; RawMonadPlus; RawMonadT)
open import Function.Base using (_∘′_; const; _$_)
open import Level using (Level; _⊔_; suc)
open import Level using (Level)

private
variable
Expand Down