diff options
Diffstat (limited to 'src/eval.c')
| -rw-r--r-- | src/eval.c | 18 |
1 files changed, 18 insertions, 0 deletions
@@ -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; } |
