From 407a2a4a0a440c41adc19fbe8b67283b7b7c65ab Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Mon, 19 Feb 2024 12:57:26 +0100
Subject: core syntax, semantic domain, evaluation

---
 lib/Syntax.ml | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 lib/Syntax.ml

(limited to 'lib/Syntax.ml')

diff --git a/lib/Syntax.ml b/lib/Syntax.ml
new file mode 100644
index 0000000..6cd988a
--- /dev/null
+++ b/lib/Syntax.ml
@@ -0,0 +1,19 @@
+type tm =
+  | Var of int
+  | Pi of tm * (* BINDS *) tm
+  | Lam of (* BINDS *) tm
+  | App of tm * tm
+  | Sg of tm * (* BINDS *) tm
+  | Pair of tm * tm
+  | Fst of tm
+  | Snd of tm
+  | Type
+  | Bool
+  | True
+  | False
+  | BoolElim of {
+      motive : (* BINDS *) tm;
+      true_case : tm;
+      false_case : tm;
+      scrut : tm;
+    }
-- 
cgit 1.4.1