From 6b7f7a0ad56a9500f592180c7b7c91b2b6a9acb9 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sat, 17 Dec 2022 17:36:21 +0000
Subject: Define substitution interfaces.

---
 obs.ipkg                 |  1 +
 src/Obs/Substitution.idr | 11 +++++++++++
 2 files changed, 12 insertions(+)
 create mode 100644 src/Obs/Substitution.idr

diff --git a/obs.ipkg b/obs.ipkg
index 93c47b7..1ae6e84 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -12,5 +12,6 @@ modules
   , Obs.Main
   , Obs.Parser
   , Obs.Sort
+  , Obs.Substitution
   , Obs.Syntax
   , Obs.Term
diff --git a/src/Obs/Substitution.idr b/src/Obs/Substitution.idr
new file mode 100644
index 0000000..914e612
--- /dev/null
+++ b/src/Obs/Substitution.idr
@@ -0,0 +1,11 @@
+module Obs.Substitution
+
+import Data.Fin
+
+public export
+interface Rename (x : Nat -> Type) where
+  rename : forall m, n . x n -> (Fin n -> Fin m) -> x m
+
+public export
+interface Subst (x, y, z : Nat -> Type) where
+  subst : forall m, n . x n -> (Fin n -> y m) -> z m
-- 
cgit v1.2.3