From 137962c1760c396f9960591af42b5a01f16ae7bd Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 27 Mar 2023 00:07:39 +0200
Subject: [PATCH] add missing %default total

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

diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index fed340c..0248a21 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -6,6 +6,8 @@ import public Control.Monad.Either
 import public Control.Monad.Reader
 import Data.Maybe
 
+%default total
+
 
 public export
 record CmpContext where
@@ -98,7 +100,7 @@ parameters (defs : Definitions' q g)
   ||| * all equality types are subsingletons because uip is admissible by
   |||   boundary separation.
   ||| * an enum type is a subsingleton if it has zero or one tags.
-  public export
+  public export covering
   isSubSing : HasErr q m => {n : Nat} -> Term q 0 n -> m Bool
   isSubSing ty = do
     Element ty nc <- whnfT defs ty