From 77d68435806e5a4c1f9e8c30d69d8d033539c570 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 31 Mar 2023 16:44:02 +0100
Subject: Define Terms.

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

(limited to 'src/Core')

diff --git a/src/Core/Term.idr b/src/Core/Term.idr
new file mode 100644
index 0000000..603d8a9
--- /dev/null
+++ b/src/Core/Term.idr
@@ -0,0 +1,20 @@
+module Core.Term
+
+import Core.Context
+import Core.Var
+
+%prefix_record_projections off
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Term : Context -> Type where
+  Var : Var sx -> Term sx
+
+  Set : Term sx
+
+  Pi : (n : Name) -> Term sx -> Term (sx :< n) -> Term sx
+  Abs : (n : Name) -> Term (sx :< n) -> Term sx
+  App : Term sx -> Term sx -> Term sx
+
+%name Term t, u, v
-- 
cgit v1.2.3