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