public interface GoalChooser
Modifier and Type | Method and Description |
---|---|
Goal |
getNextGoal() |
void |
init(Proof p_proof,
ImmutableList<Goal> p_goals)
Initialise this DefaultGoalChooser for use with a given Proof and a list of goals.
|
void |
removeGoal(Goal p_goal)
Remove p_goal from selectedList (e.g. no taclet can be applied to
p_goal)
|
void |
updateGoalList(Node node,
ImmutableList<Goal> newGoals)
The given node has become an internal node of the proof tree, and the
children of the node are the given goals
|
void init(Proof p_proof, ImmutableList<Goal> p_goals)
p_proof
- *param p_goals the initial list of goalsGoal getNextGoal()
void removeGoal(Goal p_goal)
void updateGoalList(Node node, ImmutableList<Goal> newGoals)
node
- newGoals
-