Package | Description |
---|---|
de.uka.ilkd.key.macros.scripts |
Proof script commands are a simple proof automation facility.
|
Modifier and Type | Field and Description |
---|---|
java.lang.String |
SaveNewNameCommand.Parameters.abbreviation |
boolean |
SMTCommand.SMTCommandArguments.allGoals |
java.lang.Boolean |
TryCloseCommand.TryCloseArguments.assertClosed |
java.lang.String |
SelectCommand.Parameters.branch
The name of the branch to select
|
java.lang.String |
TryCloseCommand.TryCloseArguments.branch |
java.lang.String |
AutoCommand.Parameters.breakpoint
Run on formula matching the given regex
|
java.lang.String |
SetEchoCommand.Parameters.command
The command: "on" or "off".
|
java.lang.String |
SetFailOnClosedCommand.Parameters.command
The command: "on" or "off".
|
java.lang.String |
ScriptCommand.Parameters.filename |
Term |
RewriteCommand.Parameters.find
Term, which should be replaced
|
Term |
AssumeCommand.FormulaParameter.formula |
Term |
RuleCommand.Parameters.formula |
Term |
SelectCommand.Parameters.formula
A formula defining the goal to select
|
Term |
AxiomCommand.FormulaParameter.formula |
Term |
InstantiateCommand.Parameters.formula |
Term |
RewriteCommand.Parameters.formula
Formula, where to find
find . |
Term |
CutCommand.Parameters.formula |
java.lang.Integer |
AssertCommand.Parameters.goals
The number of open and enabled goals.
|
java.lang.String |
InstantiateCommand.Parameters.hide |
java.lang.String |
SetCommand.Parameters.key
Normal key-value setting -- key
|
java.lang.String |
MacroCommand.Parameters.macroName
Macro name parameter
|
java.lang.String |
MacroCommand.Parameters.matches
Run on formula matching the given regex
|
java.lang.String |
RuleCommand.Parameters.matches
Represents a part of a formula (may use Java regular expressions as
long as supported by proof script parser).
|
java.lang.String |
AutoCommand.Parameters.matches
Run on formula matching the given regex
|
java.lang.String |
SaveNewNameCommand.Parameters.matches |
int |
AutoCommand.Parameters.maxSteps |
java.lang.String |
EchoCommand.Parameters.message
The message to show.
|
java.lang.Integer |
SelectCommand.Parameters.number
The number of the goal to select, starts with 0.
|
java.lang.Integer |
MacroCommand.Parameters.occ
Run on formula number "occ" parameter
|
int |
RuleCommand.Parameters.occ |
int |
InstantiateCommand.Parameters.occ |
Term |
RuleCommand.Parameters.on |
boolean |
AutoCommand.Parameters.onAllOpenGoals |
java.lang.Boolean |
SetCommand.Parameters.oneStepSimplification
One Step Simplification parameter
|
java.lang.Integer |
SetCommand.Parameters.proofSteps
Maximum number of proof steps parameter
|
Term |
RewriteCommand.Parameters.replace
Substitutent
|
java.lang.String |
RuleCommand.Parameters.rulename |
java.lang.String |
JavascriptCommand.Parameters.script |
java.lang.String |
SMTCommand.SMTCommandArguments.solver |
java.lang.Integer |
TryCloseCommand.TryCloseArguments.steps |
java.lang.String |
SchemaVarCommand.Parameters.type |
java.lang.String |
SetCommand.Parameters.value
Normal key-value setting -- value
|
java.lang.String |
SchemaVarCommand.Parameters.var |
java.lang.String |
InstantiateCommand.Parameters.var |
Term |
InstantiateCommand.Parameters.with |
Copyright © 2003-2019 The KeY-Project.