@FunctionalInterface
public static interface Provers.UseWhenPossibleListener
Modifier and Type | Method and Description |
---|---|
boolean |
loadExtra(mmj.transforms.WorksheetInfo info,
ParseNode root,
Prover.HypProverResult r)
If
assrt has extra variables in the hypotheses (such as
filling a goal "A = C" with transitivity "A = B & B = C => A = C", in
which the variable B is not present in the conclusion), the initial
goal matching will not be sufficient to fill all the steps, and an
IllegalArgumentException will be triggered. |
boolean loadExtra(mmj.transforms.WorksheetInfo info, ParseNode root, Prover.HypProverResult r)
assrt
has extra variables in the hypotheses (such as
filling a goal "A = C" with transitivity "A = B & B = C => A = C", in
which the variable B is not present in the conclusion), the initial
goal matching will not be sufficient to fill all the steps, and an
IllegalArgumentException
will be triggered. To prevent this,
subclasses should override this method and fill these extra variables
based on domain-specific rules. If this method does nothing, this
class will perform the same function as Provers.UseWhenPossible
.info
- The contextroot
- The goalr
- The partially filled result (r.subst
contains nulls,
which should be set by this method)