From fd658831ab53f07969524fee0257d086d6f79f5a Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Wed, 12 Jul 2023 14:02:42 +0100
Subject: Prove unification correct.

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

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

diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index ebb7b00..b65859e 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -1,7 +1,8 @@
 module Data.Term
 
-import public Data.Vect
+import public Data.DPair
 import public Data.Fin.Strong
+import public Data.Vect
 import Data.Vect.Properties.Map
 import Syntax.PreorderReasoning
 
@@ -15,6 +16,10 @@ record Signature where
 
 %name Signature sig
 
+public export
+(.Op) : Signature -> Type
+sig .Op = Exists sig.Operator
+
 public export
 data Term : Signature -> Nat -> Type where
   Var : SFin (S n) -> Term sig (S n)
@@ -98,6 +103,12 @@ export
 opInjectiveLen : (prf : Op {k} op ts = Op {k = n} op' us) -> k = n
 opInjectiveLen Refl = Refl
 
+export
+opInjectiveOp :
+  (prf : Op {sig, k} op ts = Op {sig, k = n} op' us) ->
+  the sig.Op (Evidence k op) = Evidence n op'
+opInjectiveOp Refl = Refl
+
 export
 opInjectiveTs' : {0 ts, us : Vect k (Term sig n)} -> (prf : Op op ts = Op op us) -> ts = us
 opInjectiveTs' Refl = Refl
-- 
cgit v1.2.3