From 688204f1a4d06aab1ca4f1ae06093be5dab7b584 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 24 Aug 2023 17:45:20 +0200
Subject: [PATCH] make some things private

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

diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr
index cd4cd98..460d951 100644
--- a/lib/Quox/Reduce.idr
+++ b/lib/Quox/Reduce.idr
@@ -219,23 +219,23 @@ mutual
   isRedexT _    _          = False
 
 
-public export
+private
 tycaseRhs : (k : TyConKind) -> TypeCaseArms d n ->
             Maybe (ScopeTermN (arity k) d n)
 tycaseRhs k arms = lookupPrecise k arms
 
-public export
+private
 tycaseRhsDef : Term d n -> (k : TyConKind) -> TypeCaseArms d n ->
                ScopeTermN (arity k) d n
 tycaseRhsDef def k arms = fromMaybe (SN def) $ tycaseRhs k arms
 
-public export
+private
 tycaseRhs0 : (k : TyConKind) -> TypeCaseArms d n ->
              (0 eq : arity k = 0) => Maybe (Term d n)
 tycaseRhs0 k arms {eq} with (tycaseRhs k arms) | (arity k)
   tycaseRhs0 k arms {eq = Refl} | res | 0 = map (.term) res
 
-public export
+private
 tycaseRhsDef0 : Term d n -> (k : TyConKind) -> TypeCaseArms d n ->
                 (0 eq : arity k = 0) => Term d n
 tycaseRhsDef0 def k arms = fromMaybe def $ tycaseRhs0 k arms