Define Terms.

2 files changed, 22 insertions, 0 deletions

diff --git a/obs.ipkg b/obs.ipkg
index 835638d..c225c40 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -2,4 +2,9 @@ package obs
 authors = "Greg Brown"
 sourcedir = "src"
 
+depends = contrib
+
 options = "--total"
+
+modules
+  = Core.Term
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