From d2bd03a17e23153b42bdb15ec041595f6594e14c Mon Sep 17 00:00:00 2001
From: xenia <xenia.agda@gmail.com>
Date: Sun, 3 Sep 2023 13:50:30 +0200
Subject: [PATCH] infix or-else

---
 src/Base.agda       | 2 ++
 src/Parse-HTTP.agda | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

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 ]