SIGNAL
)Proof Status has changed
GET
)Proof node information
input
::=
#node
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"result" |
string | Proof node title |
"proved" |
boolean | Proof node complete |
"pending" |
number | Pending children |
"size" |
number | Proof size |
"stats" |
string | Node statistics |
signals
plugins.wp.tip.proofStatus
GET
)Current Proof Status of a Goal
input
::=
goal
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"current" |
#node |
Current proof node |
"parents" |
#node
[] |
Proof node parents |
"pending" |
number | Pending proof nodes |
"index" |
number | Current node index among pending nodes (else -1) |
"results" |
[ prover , result ]
[] |
Prover results for current node |
"tactic" |
string | Proof node tactic header (if any) |
"children" |
[ string ,
#node ] [] |
Proof node tactic children (id any) |
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
)Remove node from tree and go to parent
input
::=
#node
output
::=
null
SIGNAL
)Updated TIP printer
DATA
)Integer constants format
iformat
::=
"dec"
|"hex"
|"bin"
DATA
)Real constants format
rformat
::=
"ratio"
|"float"
|"double"
EXEC
)Pretty-print the associated node
input
::=
{
input…}
output
::=
text
Input | Format | Description |
---|---|---|
"node" |
#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 |