From 195791e158c77d64cf709bad370c9c65a175c845 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 19 Feb 2023 17:43:27 +0100
Subject: [PATCH] export isSubSing

---
 lib/Quox/Equal.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index ba5fd48..81bbbf9 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -80,7 +80,7 @@ parameters (defs : Definitions' q g)
   ||| * a pair type is a subsingleton if both its elements are.
   ||| * all equality types are subsingletons because uip is admissible by
   |||   boundary separation.
-  private
+  public export
   isSubSing : Term q 0 n -> Bool
   isSubSing ty =
     let Element ty nc = whnfD defs ty in