public class TacletAppIntermediate extends AppIntermediate
Modifier and Type | Field and Description |
---|---|
private ImmutableList<String> |
ifDirectFormulaList |
private ImmutableList<String> |
ifSeqFormulaList |
private LinkedList<String> |
insts |
private ImmutableList<Name> |
newNames |
private Pair<Integer,PosInTerm> |
posInfo |
private String |
tacletName |
Constructor and Description |
---|
TacletAppIntermediate(String tacletName,
Pair<Integer,PosInTerm> posInfo,
LinkedList<String> insts,
ImmutableList<String> ifSeqFormulaList,
ImmutableList<String> ifDirectFormulaList,
ImmutableList<Name> newNames)
Constructs a new intermediate taclet application.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<String> |
getIfDirectFormulaList() |
ImmutableList<String> |
getIfSeqFormulaList() |
LinkedList<String> |
getInsts() |
ImmutableList<Name> |
getNewNames() |
Pair<Integer,PosInTerm> |
getPosInfo() |
String |
getRuleName() |
getLineNr, setLineNr
private String tacletName
private LinkedList<String> insts
private ImmutableList<String> ifSeqFormulaList
private ImmutableList<String> ifDirectFormulaList
private ImmutableList<Name> newNames
public TacletAppIntermediate(String tacletName, Pair<Integer,PosInTerm> posInfo, LinkedList<String> insts, ImmutableList<String> ifSeqFormulaList, ImmutableList<String> ifDirectFormulaList, ImmutableList<Name> newNames)
tacletName
- Name of the taclet.posInfo
- Position information (Integer representing position
of the target formula, PosInTerm for relevant term inside the formula).insts
- Schema variable instantiations.ifSeqFormulaList
- ifDirectFormulaList
- newNames
- New names registered during taclet application.public String getRuleName()
getRuleName
in class AppIntermediate
public LinkedList<String> getInsts()
public ImmutableList<String> getIfSeqFormulaList()
public ImmutableList<String> getIfDirectFormulaList()
public ImmutableList<Name> getNewNames()
getNewNames
in class AppIntermediate