diff options
Diffstat (limited to 'lib/types.ml')
| -rw-r--r-- | lib/types.ml | 9 |
1 files changed, 8 insertions, 1 deletions
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 |