infix or-else

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) = ⊤

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 ]