1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
\DOC print_state
\TYPE {print_state : (int -> void)}
\SYNOPSIS
Prints the top levels of the subgoal package goal stack.
\DESCRIBE
The function {print_state} is part of the subgoal package. Calling
{print_state n} prints the top {n} levels of the goal stack of the current
proof state (that is, the top {n} levels of unproven subgoals). If more than
one subgoal is produced, they are printed from the bottom of the stack so that
the current goal is printed last. If {n} is negative or is greater than the
number of levels on the goal stack, the whole stack is printed. If no goal has
been set or {n} is zero, nothing will be printed. If the original goal has just
been proved so that the proof state consists of a theorem, and {n} is non-zero,
{goal proved} is printed. For a description of the subgoal package, see
{set_goal}.
\FAILURE
Never fails.
\EXAMPLE
{
#g "(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])";;
"(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])"
() : void
#e CONJ_TAC;;
OK..
2 subgoals
"TL[1;2;3] = [2;3]"
"HD[1;2;3] = 1"
() : void
#print_state 2;;
"(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])"
2 subgoals
"TL[1;2;3] = [2;3]"
"HD[1;2;3] = 1"
() : void
}
\USES
Examining the proof state during an interactive proof session.
\SEEALSO
b, backup, backup_limit, e, expand, expandf, g, get_state, p, r,
rotate, save_top_thm, set_goal, set_state, top_goal, top_thm.
\ENDDOC
|
