diff --git a/src/Base.agda b/src/Base.agda index 3378e8a..a2bf003 100644 --- a/src/Base.agda +++ b/src/Base.agda @@ -38,6 +38,8 @@ _or-else_ : {A : Type} → Maybe A → A → A (real x) or-else _ = x cake or-else x = x +infix 10 _or-else_ + is-real : {A : Type} → Maybe A → Type is-real cake = ⊥ is-real (real x) = ⊤ diff --git a/src/Parse-HTTP.agda b/src/Parse-HTTP.agda index 07eaed2..d7c2a85 100644 --- a/src/Parse-HTTP.agda +++ b/src/Parse-HTTP.agda @@ -138,7 +138,7 @@ module Parse-URL where reg-name = decode-utf8⁺ <$?>′ (many (unreserved <|>′ percent-encoded <|>′ sub-delims)) unchecked : [ Parser Authority ] - unchecked = (λ (host , rest) → host ꞉ (proj₂ <$> rest) or-else 80) + unchecked = (λ (host , rest) → host ꞉ (proj₂ <$> rest or-else 80)) <$>′ (reg-name <&?>′ enbox (any-of ":" <&>′ enbox number)) parse-path : [ Parser Path ]