From 42c2217907e9092960d5c67a6d89b94306d94cb2 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 23 May 2024 23:27:00 +0200
Subject: [PATCH] Eq/Ord/Show for No

---
 lib/Quox/No.idr | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/lib/Quox/No.idr b/lib/Quox/No.idr
index 4134485..508e31a 100644
--- a/lib/Quox/No.idr
+++ b/lib/Quox/No.idr
@@ -13,6 +13,10 @@ data No : Pred Bool where
 
 export Uninhabited (No True) where uninhabited _ impossible
 
+export Eq   (No p) where _ == _ = True
+export Ord  (No p) where compare _ _ = EQ
+export Show (No p) where showPrec _ _ = "Ah"
+
 export %inline
 soNo : So b -> No b -> Void
 soNo Oh Ah impossible