summaryrefslogtreecommitdiff
path: root/proposition.h
diff options
context:
space:
mode:
authorKai Stevenson <kai@kaistevenson.com>2023-06-11 23:33:40 -0700
committerKai Stevenson <kai@kaistevenson.com>2023-06-11 23:33:40 -0700
commit43bfe5935b3f1d38775c3bc65262aca5683c0fb5 (patch)
treec2290c617bc40cc5f4a33c56d54548a6d9084253 /proposition.h
parentd063e3c2c6f4b1566c28d0ea92186f356017f99f (diff)
added parsing of justifications
Diffstat (limited to 'proposition.h')
-rw-r--r--proposition.h19
1 files changed, 18 insertions, 1 deletions
diff --git a/proposition.h b/proposition.h
index d2f5ac6..95f377c 100644
--- a/proposition.h
+++ b/proposition.h
@@ -10,7 +10,24 @@ typedef struct Proposition {
} prop_t;
prop_t init_prop(prop_t* propA, prop_t* propB, tokenType_t relation);
prop_t init_simple_prop(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 {
- tokenType_t rule;
+ justRule_t rule;
+ int* references;
+ int referencesCount;
} just_t;
+just_t init_just(justRule_t rule, int* references, int referencesCount);
#endif