1 files changed, 22 insertions, 0 deletions
diff --git a/src/Core/Term/NormalForm.idr b/src/Core/Term/NormalForm.idr
new file mode 100644
index 0000000..9984bee
--- /dev/null
+++ b/src/Core/Term/NormalForm.idr
@@ -0,0 +1,22 @@
+module Core.Term.NormalForm
+
+import Core.Term
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Neutral : Term n -> Type where
+  Var : Neutral (Var i)
+  App : Neutral t -> Neutral (App t u)
+
+public export
+data Whnf : Term n -> Type where
+  Ntrl : Neutral t -> Whnf t
+
+  Set : Whnf Set
+
+  Pi : Whnf (Pi a b)
+  Abs : Whnf (Abs t)
+
+%name Neutral n, m
+%name Whnf n, m