From c62b9753293389c37f29089a856a5d9a42ea23d5 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 1 Apr 2023 13:16:22 +0100
Subject: Define Neutrals and Whnfs.

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

(limited to 'src')

diff --git a/src/Core/Term/NormalForm.idr b/src/Core/Term/NormalForm.idr
new file mode 100644
index 0000000..14a3f20
--- /dev/null
+++ b/src/Core/Term/NormalForm.idr
@@ -0,0 +1,25 @@
+module Core.Term.NormalForm
+
+import Core.Context
+import Core.Term
+import Core.Var
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Neutral : Term sx -> Type where
+  Var : Neutral (Var v)
+
+  App : Neutral t -> Neutral (App t u)
+
+public export
+data Whnf : Term sx -> Type where
+  Ntrl : Neutral t -> Whnf t
+
+  Set : Whnf Set
+
+  Pi : Whnf (Pi n t u)
+  Abs : Whnf (Abs n t)
+
+%name Neutral n, m
+%name Whnf n, m
-- 
cgit v1.2.3