diff --git a/flake.nix b/flake.nix index e57c15d..119beba 100644 --- a/flake.nix +++ b/flake.nix @@ -22,6 +22,9 @@ mkdir -p ./artifacts ${agda}/bin/agda --compile-dir ./artifacts --compile "''${1:-./Main.agda}" } + clean() { + fd -I '.agdai|artifacts' --exec rm -rf + } ''; henttp = pkgs.stdenv.mkDerivation { diff --git a/src/Main.agda b/src/Main.agda index 90aa188..8c8f5bb 100644 --- a/src/Main.agda +++ b/src/Main.agda @@ -21,12 +21,6 @@ open import NonEmpty open import Parse-HTTP 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 content-type content = UTF-8.encode-string (String.toList (headers String.++ "\r\n\r\n")) ++ content where