Wp.ProverSearch
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