1 files changed, 20 insertions, 0 deletions
diff --git a/src/nbe/Syntax.ml b/src/nbe/Syntax.ml
new file mode 100644
index 0000000..dd690fb
--- /dev/null
+++ b/src/nbe/Syntax.ml
@@ -0,0 +1,20 @@
+type t = Data.syn =
+  | Var of int
+  | Pi of Ident.local * t * (* BINDS *) t
+  | Lam of Ident.local * (* BINDS *) t
+  | App of t * t
+  | Sg of Ident.local * t * (* BINDS *) t
+  | Pair of t * t
+  | Fst of t
+  | Snd of t
+  | Type
+  | Bool
+  | True
+  | False
+  | BoolElim of {
+      motive_var : Ident.local;
+      motive : (* BINDS *) t;
+      true_case : t;
+      false_case : t;
+      scrut : t;
+    }