module ProofScript:sig
..end
class console :title:string ->
Tactical.feedback
typejscript =
alternative list
type
alternative = private
| |
Prover of |
|||
| |
Tactic of |
(* | With number of pending goals | *) |
| |
Error of |
type
jtactic = {
|
header : |
|
tactic : |
|
params : |
|
select : |
val is_prover : alternative -> bool
val is_tactic : alternative -> bool
val a_prover : VCS.prover -> VCS.result -> alternative
val a_tactic : jtactic ->
(string * jscript) list -> alternative
val pending : alternative -> int
pending goals
val status : jscript -> int
minimum of pending goals
val decode : Json.t -> jscript
val encode : jscript -> Json.t
val jtactic : title:string ->
Tactical.tactical -> Tactical.selection -> jtactic
val configure : jtactic ->
Conditions.sequent -> (Tactical.tactical * Tactical.selection) option
Json Codecs
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 : 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