Module Wp.ProverScriptSource

Sourcetype 'a process = ?valid:bool -> ?failed:bool -> ?scratch:bool -> ?provers:VCS.prover list -> ?depth:int -> ?width:int -> ?backtrack:int -> ?auto:Strategy.heuristic list -> ?strategies:bool -> ?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
  • valid: Play provers with valid result (default: true)
  • failed: Play provers with invalid result (default: true)
  • scratch: Discard existing script (default: false)
  • provers: Additional list of provers to try when stuck
  • depth: Strategy search depth (default: 0)
  • width: Strategy search width (default: 0)
  • backtrack: Strategy backtracking (default: 0)
  • auto: Strategies to try (default: none)
Sourceval spawn : unit process
Sourceval explore : ?depth:int -> ?strategy:ProofStrategy.strategy -> ?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
Sourceval get : Wpo.t -> [ `Script | `Proof | `Saved | `None ]