See: Description
Interface | Description |
---|---|
ProofScriptCommand<T> |
A
ProofScriptCommand is an executable mutation on the given proof. |
Class | Description |
---|---|
AbstractCommand<T> |
Inheritance:
|
ActivateCommand |
Command for re-activating the first open (not necessarily enabled)
Goal after a "leave" command. |
AssertCommand |
Halts the script if some condition is not met.
|
AssertCommand.Parameters |
The Assigned parameters (currently only the passed goals).
|
AssumeCommand |
The assume command takes one argument: * a formula to which the command is
applied
|
AssumeCommand.FormulaParameter | |
AutoCommand |
The AutoCommand invokes the automatic strategy "Auto".
|
AutoCommand.Parameters | |
AxiomCommand |
The axiom command takes one argument: a formula to which the command is
applied.
|
AxiomCommand.FormulaParameter | |
CutCommand |
The command object CutCommand has as scriptcommand name "cut"
As parameters:
a formula with the id "#2"
|
CutCommand.Parameters | |
EchoCommand |
A simple "echo" command for giving feedback to human observers during lengthy
executions.
|
EchoCommand.Parameters | |
EngineState | |
ExitCommand | |
FocusOnSelectionAndHideCommand |
Hide all formulas that are not selected
Parameter:
* The sequent with those formulas that should not be hidden
Created by sarah on 1/12/17.
|
InstantiateCommand |
instantiate var=a occ=2 with="a_8" hide
|
InstantiateCommand.Parameters | |
JavascriptCommand | |
JavascriptCommand.JavascriptInterface | |
JavascriptCommand.Parameters | |
LeaveCommand | |
LetCommand | |
MacroCommand | |
MacroCommand.Parameters | |
NoArgumentCommand | |
ProofScriptEngine | |
RewriteCommand |
This class provides the command
rewrite . |
RewriteCommand.Parameters |
Parameters for the
RewriteCommand |
RuleCommand |
Command that applies a calculus rule All parameters are passed as strings and
converted by the command.
|
RuleCommand.Parameters | |
SaveInstCommand |
Special "Let" usually to be applied immediately after a manual rule
application.
|
SaveNewNameCommand |
Special "Let" usually to be applied immediately after a manual rule
application.
|
SaveNewNameCommand.Parameters | |
SchemaVarCommand | |
SchemaVarCommand.Parameters | |
ScriptCommand | |
ScriptCommand.Parameters | |
ScriptNode | |
ScriptTreeParser | |
SelectCommand | |
SetCommand | |
SetCommand.Parameters | |
SetEchoCommand |
A simple "echo" command for giving feedback to human observers during lengthy
executions.
|
SetEchoCommand.Parameters | |
SetFailOnClosedCommand |
Sets the behavior if an already closed proof is encountered: Either throw an
exception (default behavior, sensible for specially tailored scripts for
which a prematurely closed proof is unexpected) or peacefully terminate (if
the script addresses different problems of different complexity in a
try-and-error manner, etc.).
|
SetFailOnClosedCommand.Parameters | |
SkipCommand | |
SMTCommand | |
SMTCommand.SMTCommandArguments | |
TryCloseCommand |
The script command tryclose" has two optional arguments:
steps: INTEGER number of steps to use
#2: STRING the number of the branch which should be closed
If #2 is not given or not a number, the TryClose macro is applied to all open
goals.
|
TryCloseCommand.TryCloseArguments |
Exception | Description |
---|---|
ProofAlreadyClosedException |
Thrown if during the execution of a command, the proof is already closed.
|
ScriptException |
ProofScriptCommand
,
ProofScriptEngine
,
EngineState
Copyright © 2003-2019 The KeY-Project.