sig
class console : pool:Lang.F.pool -> title:string -> Tactical.feedback
type jscript = ProofScript.alternative list
and alternative = private
Prover of VCS.prover * VCS.result
| Tactic of int * ProofScript.jtactic *
(string * ProofScript.jscript) list
| Error of string * Json.t
and jtactic = {
header : string;
tactic : string;
params : Json.t;
select : Json.t;
}
val is_prover : ProofScript.alternative -> bool
val is_tactic : ProofScript.alternative -> bool
val a_prover : VCS.prover -> VCS.result -> ProofScript.alternative
val a_tactic :
ProofScript.jtactic ->
(string * ProofScript.jscript) list -> ProofScript.alternative
val pending : ProofScript.alternative -> int
val pending_any : ProofScript.jscript -> int
val has_proof : ProofScript.jscript -> bool
val decode : Json.t -> ProofScript.jscript
val encode : ProofScript.jscript -> Json.t
val jtactic :
title:string ->
Tactical.tactical -> Tactical.selection -> ProofScript.jtactic
val configure :
ProofScript.jtactic ->
Conditions.sequent -> (Tactical.tactical * Tactical.selection) option
val json_of_selection : Tactical.selection -> Json.t
val selection_of_json : Conditions.sequent -> Json.t -> Tactical.selection
val selection_target : Json.t -> string
val json_of_param :
Tactical.tactical -> Tactical.parameter -> string * Json.t
val param_of_json :
Tactical.tactical ->
Conditions.sequent -> Json.t -> Tactical.parameter -> unit
val json_of_parameters : Tactical.tactical -> Json.t
val parameters_of_json :
Tactical.tactical -> Conditions.sequent -> Json.t -> unit
val json_of_tactic :
ProofScript.jtactic -> (string * Json.t) list -> Json.t
val json_of_result : VCS.prover -> VCS.result -> Json.t
val prover_of_json : Json.t -> VCS.prover option
val result_of_json : Json.t -> VCS.result
end