summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/eval.c18
1 files changed, 18 insertions, 0 deletions
diff --git a/src/eval.c b/src/eval.c
index 4e978b6..263e1c1 100644
--- a/src/eval.c
+++ b/src/eval.c
@@ -61,6 +61,24 @@ char just_is_sound(line_t line, lineSet_t lines) {
return 0;
}
return peq(prop, *w.propA) || peq(prop, *w.propB);
+ case IMPLICATION_ELIM:
+ wl = lines.lines[just.references[0] - 1];
+ xl = lines.lines[just.references[1] - 1];
+ w = wl.proposition;
+ x = xl.proposition;
+ if (!seqlt(line.scope, wl.scope) || !seqlt(line.scope, xl.scope)) {
+ return 0;
+ }
+ /* find the positions of the arguments */
+ if (!w.isSimple && peq(prop, *w.propB) && w.relation == IMPLICATION && peq(x, *w.propA)) {
+ return 1;
+ }
+ else if (!x.isSimple && peq(prop, *x.propB) && x.relation == IMPLICATION && peq(w, *x.propA)) {
+ return 1;
+ }
+ else {
+ return 0;
+ }
default:
return 0;
}