From 69de932f9116b30adfd689d38e35ace63aef0e2d Mon Sep 17 00:00:00 2001
From: filip <“filip.rabiega@gmail.com”>
Date: Fri, 16 Aug 2024 14:11:00 +0200
Subject: added api

---
 lib/types.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'lib/types.ml')

diff --git a/lib/types.ml b/lib/types.ml
index bf6a34d..a069cbd 100644
--- a/lib/types.ml
+++ b/lib/types.ml
@@ -12,7 +12,7 @@ type proposition =
   | Iff of proposition * proposition
 
 (* interpretation of propositional symbols *)
-type interpretation = (string * bool) list
+type interpretation = (string * bool) list (* note: we're using OCaml booleans here *)
 
 (* allows us to substitute any proposition for any atomic literal *)
 type substitution = (string * proposition) list
@@ -30,3 +30,10 @@ type tok =
   | LEFT_PAREN
   | RIGHT_PAREN
   | SKIP
+
+(* sequent *)
+type seq = Seq of proposition list * proposition list 
+
+(* tree of sequents where Conclusion(s, l) represents a sequent s and a list l of
+ * strees that together prove s *)
+type stree = Concl of seq * stree list
-- 
cgit v1.2.3