From 571471ad7ba091bee9e98cc12a97a4d185d07a3d Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 31 Mar 2023 16:45:40 +0100
Subject: Define Envs.

---
 src/Core/Term/Environment.idr | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 src/Core/Term/Environment.idr

(limited to 'src')

diff --git a/src/Core/Term/Environment.idr b/src/Core/Term/Environment.idr
new file mode 100644
index 0000000..8e7ce4f
--- /dev/null
+++ b/src/Core/Term/Environment.idr
@@ -0,0 +1,13 @@
+module Core.Term.Environment
+
+import Core.Context
+import Core.Term
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Env : Context -> Type where
+  Lin : Env [<]
+  (:<) : Env sx -> Term sx -> Env (sx :< n)
+
+%name Env env
-- 
cgit v1.2.3