From 66ab04e0bff5b233060aa3e0b739d1184b4c2611 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 14 Apr 2023 17:33:55 +0100
Subject: Define Terms.

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

(limited to 'src')

diff --git a/src/Core/Term.idr b/src/Core/Term.idr
new file mode 100644
index 0000000..7fea482
--- /dev/null
+++ b/src/Core/Term.idr
@@ -0,0 +1,17 @@
+module Core.Term
+
+import public Data.Fin
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Term : Nat -> Type where
+  Var : Fin n -> Term n
+
+  Set : Term n
+
+  Pi : Term n -> Term (S n) -> Term n
+  Abs : Term (S n) -> Term n
+  App : Term n -> Term n -> Term n
+
+%name Term t, u, v
-- 
cgit v1.2.3