summaryrefslogtreecommitdiff
path: root/lib/sequent_calculus/headers.ml
diff options
context:
space:
mode:
authorfilip <“filip.rabiega@gmail.com”>2024-08-16 14:11:00 +0200
committerfilip <“filip.rabiega@gmail.com”>2024-08-16 14:11:00 +0200
commit69de932f9116b30adfd689d38e35ace63aef0e2d (patch)
treef7e8621889d313e70186ef255fcf04fe0d55d4c3 /lib/sequent_calculus/headers.ml
parent2e893fd0df7dae8c4ae843d4a23acb098dd97aff (diff)
downloadchadprover-69de932f9116b30adfd689d38e35ace63aef0e2d.tar.gz
chadprover-69de932f9116b30adfd689d38e35ace63aef0e2d.tar.bz2
chadprover-69de932f9116b30adfd689d38e35ace63aef0e2d.zip
added apiHEADmaster
Diffstat (limited to 'lib/sequent_calculus/headers.ml')
-rw-r--r--lib/sequent_calculus/headers.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/sequent_calculus/headers.ml b/lib/sequent_calculus/headers.ml
new file mode 100644
index 0000000..0bef07a
--- /dev/null
+++ b/lib/sequent_calculus/headers.ml
@@ -0,0 +1,5 @@
+(* Sequent calculus: types and exceptions *)
+
+(* exceptions that can occur when attempting a sequent proof *)
+exception RuleNotApplicable
+exception NotProvable of string