Define environment equality.

1 files changed, 17 insertions, 0 deletions

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