summaryrefslogtreecommitdiff
path: root/src/proposition.h
diff options
context:
space:
mode:
authorKai Stevenson <kai@kaistevenson.com>2023-06-13 14:50:00 -0700
committerKai Stevenson <kai@kaistevenson.com>2023-06-13 14:50:00 -0700
commit1d3bbec4660dfe4e2117826ceef9b32758b40345 (patch)
tree7c33cdf17774a122af89f3ae7743771f047942a7 /src/proposition.h
parentcaa9d17ea794a0b4823170551545498d458e1fc2 (diff)
restructured project
Diffstat (limited to 'src/proposition.h')
-rw-r--r--src/proposition.h34
1 files changed, 34 insertions, 0 deletions
diff --git a/src/proposition.h b/src/proposition.h
new file mode 100644
index 0000000..2d09688
--- /dev/null
+++ b/src/proposition.h
@@ -0,0 +1,34 @@
+#ifndef PROPOSITION
+#define PROPOSITION
+#include "lexer.h"
+typedef struct Proposition {
+ char isSimple;
+ char isNegative;
+ struct Proposition* propA;
+ struct Proposition* propB;
+ tokenType_t relation;
+ char* name;
+} prop_t;
+prop_t init_prop(char isNegative, prop_t* propA, prop_t* propB, tokenType_t relation);
+prop_t init_simple_prop(char isNegative, char* name);
+typedef enum JustificationRule {
+ ERR_R,
+ PREMISE_R,
+ ASSUMPTION_R,
+ CONJUNCT_INTRO,
+ DISJUNCT_INTRO,
+ IMPLICATION_INTRO,
+ BI_IMPLICATION_INTRO,
+ CONJUNCT_ELIM,
+ DISJUNCT_ELIM,
+ IMPLICATION_ELIM,
+ BI_IMPLICATION_ELIM
+} justRule_t;
+char* jrtos(justRule_t rule);
+typedef struct Justification {
+ justRule_t rule;
+ int* references;
+ int referencesCount;
+} just_t;
+just_t init_just(justRule_t rule, int* references, int referencesCount);
+#endif