Minor changes for use by other projects.

1 files changed, 8 insertions, 4 deletions

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
@@ -22,6 +22,10 @@ public export
 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)
   Op : sig.Operator k -> Vect k (Term sig n) -> Term sig 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