1 files changed, 30 insertions, 0 deletions
diff --git a/src/nbe/Domain.ml b/src/nbe/Domain.ml
new file mode 100644
index 0000000..6f5e11c
--- /dev/null
+++ b/src/nbe/Domain.ml
@@ -0,0 +1,30 @@
+open Bwd
+
+type t = Data.value =
+  | Neutral of ne
+  | Pi of Ident.local * t * clo
+  | Lam of Ident.local * clo
+  | Sg of Ident.local * t * clo
+  | Pair of t * t
+  | Type
+  | Bool
+  | True
+  | False
+
+and ne = Data.ne
+and ne_head = Data.ne_head = Var of int (* De Bruijn levels *)
+and frm = Data.frm =
+  | App of t
+  | Fst
+  | Snd
+  | BoolElim of {
+      motive_var : Ident.local;
+      motive : clo;
+      true_case : t;
+      false_case: t;
+    }
+
+and env = Data.env
+and clo = Data.clo = Clo of { body : Data.syn; env : env }
+
+let var i = Neutral (Var i, Bwd.Emp)