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:)") } , _