clean
This commit is contained in:
parent
5103fc0996
commit
3216656638
|
@ -22,6 +22,9 @@
|
||||||
mkdir -p ./artifacts
|
mkdir -p ./artifacts
|
||||||
${agda}/bin/agda --compile-dir ./artifacts --compile "''${1:-./Main.agda}"
|
${agda}/bin/agda --compile-dir ./artifacts --compile "''${1:-./Main.agda}"
|
||||||
}
|
}
|
||||||
|
clean() {
|
||||||
|
fd -I '.agdai|artifacts' --exec rm -rf
|
||||||
|
}
|
||||||
'';
|
'';
|
||||||
|
|
||||||
henttp = pkgs.stdenv.mkDerivation {
|
henttp = pkgs.stdenv.mkDerivation {
|
||||||
|
|
|
@ -21,12 +21,6 @@ open import NonEmpty
|
||||||
open import Parse-HTTP
|
open import Parse-HTTP
|
||||||
import UTF-8
|
import UTF-8
|
||||||
|
|
||||||
parse-digit : [ Parser Byte ]
|
|
||||||
parse-digit = (\ b → b .value <ᵇ 58) <?>′ any₁
|
|
||||||
|
|
||||||
parse-thing : [ Parser (List⁺ Byte) ]
|
|
||||||
parse-thing = many parse-digit -- (\ (a , b) → a ∷⁺ [ b ]⁺ ) <$>′ (parse-digit <&>′ enbox parse-digit)
|
|
||||||
|
|
||||||
200-ok : String.String → List Byte → List Byte
|
200-ok : String.String → List Byte → List Byte
|
||||||
200-ok content-type content = UTF-8.encode-string (String.toList (headers String.++ "\r\n\r\n")) ++ content
|
200-ok content-type content = UTF-8.encode-string (String.toList (headers String.++ "\r\n\r\n")) ++ content
|
||||||
where
|
where
|
||||||
|
|
Loading…
Reference in New Issue
Block a user