diff options
Diffstat (limited to 'src/proof/proof_rule.h')
| -rw-r--r-- | src/proof/proof_rule.h | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index bb677bdb9..25bbf3d34 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -1406,6 +1406,15 @@ enum class PfRule : uint32_t // --------------------- // Conclusion: (Q) LFSC_RULE, + //================================================ Place holder for Alethe + // rules + // ======== Alethe rule + // Children: (P1 ... Pn) + // Arguments: (id, Q, Q', A1, ..., Am) + // --------------------- + // Conclusion: (Q) + // where Q' is the representation of Q to be printed by the Alethe printer. + ALETHE_RULE, //================================================= Unknown rule UNKNOWN, |