summaryrefslogtreecommitdiff
path: root/src/Core
diff options
context:
space:
mode:
Diffstat (limited to 'src/Core')
-rw-r--r--src/Core/Term/Environment.idr13
1 files changed, 13 insertions, 0 deletions
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