1 files changed, 17 insertions, 0 deletions
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