From 11cc587d1b4a7651ea4034c5a4f86192f0ee6ece Mon Sep 17 00:00:00 2001
From: xenia <xenia.agda@gmail.com>
Date: Sat, 9 Sep 2023 13:01:12 +0200
Subject: [PATCH] Clean up imports

---
 src/Base.agda            | 5 +++--
 src/NonEmpty.agda        | 8 +++++++-
 src/Parse-HTTP/Test.agda | 4 ++--
 3 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/src/Base.agda b/src/Base.agda
index 8136755..a767012 100644
--- a/src/Base.agda
+++ b/src/Base.agda
@@ -3,6 +3,7 @@ open import Data.Bool
 open import Data.Empty
 open import Data.Unit
 open import Data.Nat
+
 import Data.String as S
 import Data.List as L
 open S using (String)
@@ -76,8 +77,8 @@ instance
   EqCh : Eq Data.Char.Char
   EqCh ._==_ a b = a Data.Char.== b
 
-  EqString : Eq Data.String.String
-  EqString ._==_ a b = a Data.String.== b
+  EqString : Eq String
+  EqString ._==_ a b = a S.== b
 
   EqMaybe : {T : Type} → ⦃ Eq T ⦄ → Eq (Maybe T)
   EqMaybe ._==_ (real a) (real b) = a == b
diff --git a/src/NonEmpty.agda b/src/NonEmpty.agda
index 395d08a..811fc48 100644
--- a/src/NonEmpty.agda
+++ b/src/NonEmpty.agda
@@ -4,7 +4,13 @@ open import Data.Product
 open import Data.Nat
 open import Data.List using (List; []; _∷_)
 open import Data.Bool
+
+import Data.String as S
+import Data.List as L
 import Data.Vec as V
+open S using (String)
+open L using (List)
+open V using (Vec)
 
 open import Base
 
@@ -62,7 +68,7 @@ list-to-list⁺? (x ∷ xs) = real (cons⁺ x xs)
 
 instance
   ShowList⁺ : {A : Type} → ⦃ Show A ⦄ → Show (List⁺ A)
-  ShowList⁺ .show x = show (list⁺-to-list x) String.++ "⁺"
+  ShowList⁺ .show x = show (list⁺-to-list x) S.++ "⁺"
     where
       import Data.String as String
 
diff --git a/src/Parse-HTTP/Test.agda b/src/Parse-HTTP/Test.agda
index 1bb0c55..f81bee5 100644
--- a/src/Parse-HTTP/Test.agda
+++ b/src/Parse-HTTP/Test.agda
@@ -108,8 +108,8 @@ module Test-HTTP where
                    ; version = HTTP11
                    ; headers =
                      record { name = string-to-ascii-list⁺ "Content-Length" ; value = string-to-ascii-list⁺ "6" }
-                     List.∷ record { name = string-to-ascii-list⁺ "Host" ; value = string-to-ascii-list⁺ "agda.nu" }
-                     List.∷ List.[]
+                     L.∷ record { name = string-to-ascii-list⁺ "Host" ; value = string-to-ascii-list⁺ "agda.nu" }
+                     L.∷ L.[]
                    ; content = real (string-to-ascii-list "mjau:)")
                    }
                  , _