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.

---
 src/Obs/Substitution.idr | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 src/Obs/Substitution.idr

(limited to 'src/Obs')

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