string-to-ascii-list function

src/Parse-HTTP/Helpers.agda

@@ -59,6 +59,9 @@ string-to-ascii-list⁺ s {ascii} {nonempty} = vec-to-list⁺ v
     v : Vec Byte (suc (pred (length s)))
     v = subst (λ x → Vec Byte x) (sym (suc[pred[n]]≡n {length s} len≢0)) (string-to-ascii-vec s {ascii})
 
+string-to-ascii-list : (s : String) → {string-is-ascii s} → List Byte
+string-to-ascii-list s {ascii} = V.toList (string-to-ascii-vec s {ascii})
+
 any-of : String → [ Parser Byte ]
 any-of x = L.foldr (λ ch p → ((_is ch) <?>′ any₁) <|>′ p) fail (S.toList x)
 

src/Parse-HTTP/Test.agda

@@ -110,7 +110,7 @@ module Test-HTTP where
                      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.[]
-                   ; content = real (list⁺-to-list (string-to-ascii-list⁺ "mjau:)"))
+                   ; content = real (string-to-ascii-list "mjau:)")
                    }
                  , _
                  , enc "\r\n"