Clean up imports

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 : Eq String
-  EqString ._==_ a b = a Data.String.== b
+  EqString ._==_ a b = a S.== b
 
   EqMaybe : {T : Type} → ⦃ Eq T ⦄ → Eq (Maybe T)
   EqMaybe ._==_ (real a) (real b) = a == 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
 

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" }
+                     L.∷ record { name = string-to-ascii-list⁺ "Host" ; value = string-to-ascii-list⁺ "agda.nu" }
-                     List.∷ List.[]
+                     L.∷ L.[]
                    ; content = real (string-to-ascii-list "mjau:)")
                    }
                  , _