Interface

class RuleMatcher

Bases: ABC

abstractmethod match_theorem(rule, proof)

Match all dependencies created by the given rule given the existing dependency graph.

Return type:

set[Assumption | NumericalCheck | RuleApplication | ARDeduction | CircleMerge | LineMerge | DirectConsequence | Reflexivity]