module ApplyResult:sig
..end
Tactic application results
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced.
type
apply_result
val get_num_subgoals : apply_result -> int
The number of Subgoals.
val get_subgoals : apply_result -> Goal.goal list
Retrieves the subgoals from the apply_result.
val get_subgoal : apply_result -> int -> Goal.goal
Retrieves a subgoal from the apply_result.
val convert_model : apply_result -> int -> Model.model -> Model.model
Convert a model for a subgoal into a model for the original
goal g
, that the ApplyResult was obtained from.
#return A model for g
val to_string : apply_result -> string
A string representation of the ApplyResult.