public class StateExpansionAndInfFlowContractApplicationMacro extends SequentialProofMacro
ProofMacro.ProgressBarListener
Constructor and Description |
---|
StateExpansionAndInfFlowContractApplicationMacro() |
Modifier and Type | Method and Description |
---|---|
boolean |
canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
|
protected ProofMacro[] |
createProofMacroArray()
Creates the proof macro array.
|
java.lang.String |
getCategory()
Gets the category of this macro.
|
java.lang.String |
getDescription()
Gets the description of this macro.
|
java.lang.String |
getName()
Gets the name of this macro.
|
applyTo, getProofMacros
applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter
public StateExpansionAndInfFlowContractApplicationMacro()
public java.lang.String getName()
ProofMacro
null
constant stringpublic java.lang.String getCategory()
ProofMacro
null
if no submenu is to be created.null
public java.lang.String getDescription()
ProofMacro
null
constant stringprotected ProofMacro[] createProofMacroArray()
SequentialProofMacro
createProofMacroArray
in class SequentialProofMacro
public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc)
This compound macro is applicable if and only if the first macro is applicable. If there is no first macro, this is not applicable.
This compound macro is applicable if and only if the first macro is applicable. If there is no first macro, this is not applicable.
canApplyTo
in interface ProofMacro
canApplyTo
in class SequentialProofMacro
proof
- the current Proof
(not null
)goals
- the goals (not null
)posInOcc
- the position in occurrence (may be null
)true
, if the macro is allowed to be applied