From a90932302afa9e13b8ed6f1159fbe604c89d453f Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 1 Apr 2023 15:13:36 +0100
Subject: Define environment equality.

---
 src/Core/Term/Environment.idr | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'src')

diff --git a/src/Core/Term/Environment.idr b/src/Core/Term/Environment.idr
index 62e3b60..4f167f9 100644
--- a/src/Core/Term/Environment.idr
+++ b/src/Core/Term/Environment.idr
@@ -41,3 +41,20 @@ index : Env sx -> Var sx -> Term sx
 index env i =
   let MkRes val thin = doIndex env $ view i in
   wkn val thin
+
+-- Equality --------------------------------------------------------------------
+
+namespace Eq
+  public export
+  data EnvEq : Env sx -> Env sx -> Type where
+    Lin : EnvEq [<] [<]
+    Add :
+      EnvEq env1 env2 ->
+      Term.wkn t thin1 = wkn u thin2 ->
+      EnvEq (Add env1 thin1 t) (Add env2 thin2 u)
+
+  %name EnvEq prf
+
+  public export
+  (:<) : EnvEq env1 env2 -> (0 t : Term sx) -> EnvEq (env1 :< t) (env2 :< t)
+  prf :< t = Add prf Refl
-- 
cgit v1.2.3