SIGNAL
)Proof Status has changed
SIGNAL
)Updated TIP printer
DATA
)Proof Node index
node
::=
#node
DATA
)Tactic identifier
tactic
::=
$tactic
GET
)Proof node information
input
::=
node
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"title" |
string | Proof node title |
"proved" |
boolean | Proof node complete |
"pending" |
number | Pending children |
"size" |
number | Proof size |
"stats" |
string | Node statistics |
"results" |
[ prover , result ]
[] |
Prover results for current node |
"tactic" (opt.) |
tactic |
Applied tactic (if any) |
"header" (opt.) |
string | Proof node tactic label (if any) |
"childLabel"
(opt.) |
string | Proof node child label (from parent, if any) |
"path" |
node [] |
Proof node path from goal |
"children" |
node [] |
Proof node tactic children (id any) |
signals
plugins.wp.tip.proofStatus
GET
)Result for specified node and prover
input
::=
{
input…}
output
::=
result
Input | Format | Description |
---|---|---|
"node" |
node |
Proof node |
"prover" |
prover |
Prover |
signals
plugins.wp.tip.proofStatus
GET
)Current Proof Status of a Goal
input
::=
{
input…}
output
::=
{
output…}
Input | Format | Description |
---|---|---|
"main" |
goal |
Proof Obligation |
"unproved" (opt.) |
boolean | Report unproved children only |
"subtree" (opt.) |
boolean | Report subtree children only |
Output | Format | Description |
---|---|---|
"size" |
number | Proof size |
"index" |
number | Current node index among pending nodes (else -1) |
"pending" |
number | Pending proof nodes |
"current" |
node |
Current proof node |
"parents" |
node [] |
parents nodes |
"tactic" (opt.) |
tactic |
Applied tactic (if any) |
"children" |
node [] |
Children nodes |
signals
plugins.wp.tip.proofStatus
SET
)Go to to first pending node, or root if none
input
::=
goal
output
::=
null
SET
)Go to root of proof tree
input
::=
goal
output
::=
null
SET
)Go to k-th pending node of proof tree
input
::=
[
goal
, number]
output
::=
null
SET
)Set current node of associated proof tree
input
::=
node
output
::=
null
SET
)Cancel all node results and sub-tree (if any)
input
::=
node
output
::=
null
SET
)Cancel node current tactic
input
::=
node
output
::=
null
SET
)Cancel parent node tactic
input
::=
node
output
::=
null
SET
)Remove the complete goal proof tree
input
::=
goal
output
::=
null
DATA
)Proof part marker
part
::=
$part
DATA
)Term marker
term
::=
$term
DATA
)Integer constants format
iformat
::=
"dec"
|"hex"
|"bin"
DATA
)Real constants format
rformat
::=
"ratio"
|"float"
|"double"
GET
)Pretty-print the associated node
input
::=
{
input…}
output
::=
text
Input | Format | Description |
---|---|---|
"node" (opt.) |
node |
Proof Node |
"indent" (opt.) |
number | Number of identation spaces |
"margin" (opt.) |
number | Maximial text width |
"iformat" (opt.) |
iformat |
Integer constants format |
"rformat" (opt.) |
rformat |
Real constants format |
"autofocus" (opt.) |
boolean | Auto-focus mode |
"unmangled" (opt.) |
boolean | Unmangled memory model |
signals
plugins.wp.tip.printStatus
SET
)Reset node selection
input
::=
node
output
::=
null
SET
)Set node selection
input
::=
{
input…}
output
::=
null
Input | Format | Description |
---|---|---|
"node" |
node |
Proof Node |
"part" (opt.) |
part |
Selected part |
"term" (opt.) |
term |
Selected term |
"extend" (opt.) |
boolean | Extending selection mode |
GET
)Get current selection in proof node
input
::=
node
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"part" (opt.) |
part |
Selected part |
"term" (opt.) |
term |
Selected term |
signals
plugins.wp.tip.printStatus
plugins.wp.tip.proofStatus
SET
)Schedule provers on proof node
input
::=
{
input…}
output
::=
null
Input | Format | Description |
---|---|---|
"node" |
node |
Proof node |
"timeout" (opt.) |
number | Prover timeout (in seconds, default: current) |
"provers" (opt.) |
prover
[] |
Prover selection (default: current |
SET
)Interrupt running provers on proof node
input
::=
{
input…}
output
::=
null
Input | Format | Description |
---|---|---|
"node" |
node |
Proof node |
"provers" (opt.) |
prover
[] |
Prover selection (default: all running provers |
SET
)Remove prover results from proof node
input
::=
{
input…}
output
::=
null
Input | Format | Description |
---|---|---|
"node" |
node |
Proof node |
"provers" (opt.) |
prover
[] |
Prover selection (default: all results |
GET
)Script Status for a given Goal
input
::=
goal
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"proof" |
boolean | Some Proof Tree can be Saved |
"script" (opt.) |
string | Script File (if any) |
"saved" |
boolean | Current Proof Script has been Saved |
signals
plugins.wp.tip.proofStatus
SET
)Save Script for the Goal
input
::=
goal
output
::=
null
SET
)Replay Saved Script for the Goal (if any)
input
::=
goal
output
::=
null
SET
)Clear Proof and Remove any Saved Script for the Goal
input
::=
goal
output
::=
null