From d42c29c3ded0e48021b24295c925b88232df6b75 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 7 Jul 2023 17:40:03 +0100
Subject: Add occurs check for terms.

---
 src/Data/Term/Zipper.idr | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src/Data/Term/Zipper.idr')

diff --git a/src/Data/Term/Zipper.idr b/src/Data/Term/Zipper.idr
index 09ba2c9..3f6668a 100644
--- a/src/Data/Term/Zipper.idr
+++ b/src/Data/Term/Zipper.idr
@@ -41,7 +41,8 @@ assoc (Op op i ts zip1) zip2 zip3 = cong (Op op i ts) (assoc zip1 zip2 zip3)
 
 -- Action ----------------------------------------------------------------------
 
-export
+-- NOTE: should this be public?
+public export
 (+) : Zipper sig n -> Term sig n -> Term sig n
 Top + t = t
 Op op i ts zip + t = Op op (insertAt i (zip + t) ts)
-- 
cgit v1.2.3