- STRUCTURE
- SYNOPSIS
Returns the current goal of the subgoal package.
- DESCRIPTION
The function top_goal is part of the subgoal package. It returns the top goal
of the goal stack in the current proof state. For a description of the subgoal
package, see set_goal.
- FAILURE
A call to top_goal will fail if there are no unproven goals. This could be
because no goal has been set using set_goal or because the last goal set has
been completely proved.
- USES
Examining the proof state after a proof fails.
- SEEALSO
set_goal,
restart,
backup,
restore,
save,
set_backup,
expand,
expandf,
p,
top_thm,
top_goal