From ea674503c0f45f9992c5668531b9acd4dab28582 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Wed, 20 Sep 2023 21:58:55 +0200
Subject: [PATCH] export PushSubsts, oops

---
 lib/Quox/Syntax/Term/Subst.idr | 1 +
 1 file changed, 1 insertion(+)

diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index 00814d8..4aa3736 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -201,6 +201,7 @@ public export
 0 CloTest : TermLike -> Type
 CloTest tm = forall d, n. tm d n -> Bool
 
+public export
 interface PushSubsts (0 tm : TermLike) (0 isClo : CloTest tm) | tm where
   pushSubstsWith : DSubst d1 d2 -> TSubst d2 n1 n2 ->
                    tm d1 n1 -> Subset (tm d2 n2) (No . isClo)