From 8c529393421843a7ccad041d2f29fa90b46bf6b6 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 30 Jun 2023 20:45:33 +0100
Subject: Define zippers and prove no cycles exist.

---
 src/Data/Term.idr | 13 +++++++++++++
 1 file changed, 13 insertions(+)

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

diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index 95fd9f8..2afc774 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -72,3 +72,16 @@ subComp :
   (r : Fin j -> Fin k) ->
   f . pure r .=. f . r
 subComp f r i = Refl
+
+-- Injectivity -----------------------------------------------------------------
+
+export
+opInjectiveLen : (prf : Op {k} op ts = Op {k = n} op' us) -> k = n
+opInjectiveLen Refl = Refl
+
+export
+opInjectiveTs :
+  {0 ts : Vect k (Term sig n)} ->
+  {0 us : Vect j (Term sig n)} ->
+  (prf : Op op ts = Op op' us) -> ts = (rewrite opInjectiveLen prf in us)
+opInjectiveTs Refl = Refl
-- 
cgit v1.2.3