module ProverScript: sig
.. end
Play provers with valid result (default: true)
type 'a
process = ?valid:bool ->
?failed:bool ->
?provers:VCS.prover list ->
?depth:int ->
?width:int ->
?backtrack:int ->
?auto:Strategy.heuristic list ->
?start:(Wpo.t -> unit) ->
?progress:(Wpo.t -> string -> unit) ->
?result:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
?success:(Wpo.t -> VCS.prover option -> unit) -> Wpo.t -> 'a
val prove : unit Task.task process
val spawn : unit process
val search : ?depth:int ->
?width:int ->
?backtrack:int ->
?auto:Strategy.heuristic list ->
?provers:VCS.prover list ->
?progress:(Wpo.t -> string -> unit) ->
?result:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
?success:(Wpo.t -> VCS.prover option -> unit) ->
ProofEngine.tree -> ProofEngine.node -> unit
val get : Wpo.t -> [ `None | `Proof | `Saved | `Script ]
val save : Wpo.t -> unit