From bb4e7c82b7ecd93b7241be5fcc547cfd282a8908 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sun, 16 Jul 2023 15:19:15 +0100
Subject: Minor changes for use by other projects.

---
 src/Data/Term.idr | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

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

diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index 01de5d2..4bb787f 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -21,6 +21,10 @@ public export
 (.Op) : Signature -> Type
 sig .Op = Exists sig.Operator
 
+public export
+interface DecOp (0 sig : Signature) where
+  decOp : (op, op' : sig.Op) -> Dec (op = op')
+
 public export
 data Term : Signature -> Nat -> Type where
   Var : SFin (S n) -> Term sig (S n)
@@ -45,7 +49,7 @@ export
 pure : (SFin k -> SFin n) -> SFin k -> Term sig n
 pure r = Var' . r
 
-export
+public export
 (<$>) : (SFin k -> Term sig n) -> Term sig k -> Term sig n
 f <$> Var i = f i
 f <$> Op op ts = Op op (map (\t => f <$> assert_smaller ts t) ts)
@@ -65,7 +69,7 @@ subCong prf (Op op ts) =
 
 -- Substitution is Monadic -----------------------------------------------------
 
-export
+public export
 (.) : (SFin k -> Term sig n) -> (SFin j -> Term sig k) -> SFin j -> Term sig n
 f . g = (f <$>) . g
 
@@ -93,8 +97,8 @@ subAssoc f g (Op op ts) = cong (Op op) $ Calc $
 
 export
 subComp :
-  (f : SFin (S k) -> Term sig n) ->
-  (r : SFin j -> SFin (S k)) ->
+  (f : SFin k -> Term sig n) ->
+  (r : SFin j -> SFin k) ->
   f . pure r .=. f . r
 subComp f r i = Refl
 
-- 
cgit v1.2.3