public class IntroducedSymbolBy extends BinaryTacletAppFeature
Modifier and Type | Field and Description |
---|---|
private Name |
ruleSetName |
private Name |
schemaVar |
private ProjectionToTerm |
term |
TOP_COST, ZERO_COST
Modifier | Constructor and Description |
---|---|
protected |
IntroducedSymbolBy(ProjectionToTerm termWithTopLevelOpToCheck,
Name ruleSetName,
Name schemaVar) |
Modifier and Type | Method and Description |
---|---|
static Feature |
create(ProjectionToTerm termWithTopLevelOpToCheck,
java.lang.String ruleSetName,
java.lang.String schemaVar) |
protected boolean |
filter(TacletApp app,
PosInOccurrence pos,
Goal goal)
Compute whether the result of the feature is zero (
true )
or infinity (false ) |
filter
computeCost
private final Name ruleSetName
private final Name schemaVar
private final ProjectionToTerm term
protected IntroducedSymbolBy(ProjectionToTerm termWithTopLevelOpToCheck, Name ruleSetName, Name schemaVar)
public static Feature create(ProjectionToTerm termWithTopLevelOpToCheck, java.lang.String ruleSetName, java.lang.String schemaVar)
protected boolean filter(TacletApp app, PosInOccurrence pos, Goal goal)
BinaryTacletAppFeature
true
)
or infinity (false
)filter
in class BinaryTacletAppFeature
app
- the TacletApppos
- position where app
is to be appliedgoal
- the goal on which app
is to be applied