Module ProverSearch

module ProverSearch: sig .. end

val first : ProofEngine.tree ->
?anchor:ProofEngine.node -> Strategy.t array -> ProofEngine.fork option
val index : ProofEngine.tree ->
anchor:ProofEngine.node -> index:int -> ProofEngine.fork option
val search : ProofEngine.tree ->
?anchor:ProofEngine.node ->
?sequent:Conditions.sequent ->
Strategy.heuristic list -> ProofEngine.fork option
val backtrack : ProofEngine.tree ->
?anchor:ProofEngine.node ->
?loop:bool -> ?width:int -> unit -> ProofEngine.fork option