diff options
Diffstat (limited to 'src/expr/proof_rule.h')
| -rw-r--r-- | src/expr/proof_rule.h | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index beff92bd4..364598cf4 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -481,11 +481,14 @@ enum class PfRule : uint32_t // ----------------------- // Conclusion: (= t1 tn) TRANS, - // ======== Congruence (subsumed by Substitute?) + // ======== Congruence // Children: (P1:(= t1 s1), ..., Pn:(= tn sn)) - // Arguments: (f) + // Arguments: (<kind> f?) // --------------------------------------------- - // Conclusion: (= (f t1 ... tn) (f s1 ... sn)) + // Conclusion: (= (<kind> f? t1 ... tn) (<kind> f? s1 ... sn)) + // Notice that f must be provided iff <kind> is a parameterized kind, e.g. + // APPLY_UF. The actual node for <kind> is constructible via + // ProofRuleChecker::mkKindNode. CONG, // ======== True intro // Children: (P:F) |