From 682965eebd27d5ffdbd1b4320e43e60ad3952ba3 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 17 Apr 2023 21:41:10 +0200
Subject: [PATCH] =?UTF-8?q?0=E2=88=A81=20is=20not=20undefined=20it's=20?=
 =?UTF-8?q?=CF=89?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 lib/Quox/Syntax/Qty.idr | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/lib/Quox/Syntax/Qty.idr b/lib/Quox/Syntax/Qty.idr
index 856c4ea..0db17b5 100644
--- a/lib/Quox/Syntax/Qty.idr
+++ b/lib/Quox/Syntax/Qty.idr
@@ -81,15 +81,12 @@ compat pi Any = True
 compat pi rh  = pi == rh
 
 
-||| "π ∧ ρ"
+||| "π ∨ ρ"
 |||
 ||| returns some quantity τ where π ≤ τ and ρ ≤ τ, if one exists.
 public export
 lub : Qty -> Qty -> Maybe Qty
-lub p q =
-  if p == Any || q == Any then Just Any
-  else if p == q then Just p
-  else Nothing
+lub p q = Just $ if p == q then p else Any
 
 
 ||| to maintain subject reduction, only 0 or 1 can occur