diff options
Diffstat (limited to 'src/proof/proof_rule.h')
| -rw-r--r-- | src/proof/proof_rule.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index d9e92fa92..eaa92c02c 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -185,6 +185,14 @@ enum class PfRule : uint32_t // where F' and G' are the result of each side of the equation above. Here, // original forms are used in a similar manner to MACRO_SR_PRED_INTRO above. MACRO_SR_PRED_TRANSFORM, + // ======== Annotation + // Children: (P1:F) + // Arguments: (a1 ... an) + // ---------------------------------------- + // Conclusion: F + // The terms a1 ... an can be anything used to annotate the proof node, one + // example is where a1 is a theory::InferenceId. + ANNOTATION, //================================================= Processing rules // ======== Remove Term Formulas Axiom // Children: none |