diff options
| author | filip <“filip.rabiega@gmail.com”> | 2024-08-16 14:11:00 +0200 |
|---|---|---|
| committer | filip <“filip.rabiega@gmail.com”> | 2024-08-16 14:11:00 +0200 |
| commit | 69de932f9116b30adfd689d38e35ace63aef0e2d (patch) | |
| tree | f7e8621889d313e70186ef255fcf04fe0d55d4c3 /lib/types.ml | |
| parent | 2e893fd0df7dae8c4ae843d4a23acb098dd97aff (diff) | |
| download | chadprover-69de932f9116b30adfd689d38e35ace63aef0e2d.tar.gz chadprover-69de932f9116b30adfd689d38e35ace63aef0e2d.tar.bz2 chadprover-69de932f9116b30adfd689d38e35ace63aef0e2d.zip | |
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 |