module S: sig .. end
type Proof.proof
val result : t -> Proof.result
val step : t -> Proof.step
val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
val compare_by_result : t -> t -> int
Compare proofs by their result
module Tbl: CCHashtbl.S with type key = t
val mk_f : Proof.step -> Proof.form -> t
Constructors and utils
In all the following constructors, theories defaults to the empty list.
Axiom constructors have default role "axiom"
val mk_f_trivial : Proof.form -> t
val mk_f_by_def : Logtk.ID.t -> Proof.form -> t
val mk_f_inference : ?check:Proof.check ->
rule:Proof.rule -> Proof.form -> Proof.parent list -> t
val mk_f_simp : ?check:Proof.check ->
rule:Proof.rule -> Proof.form -> Proof.parent list -> t
val mk_f_esa : ?check:Proof.check ->
rule:Proof.rule -> Proof.form -> Proof.parent list -> t
val mk_c : Proof.step -> SClause.t -> t
val mk_bc : Proof.step -> Proof.bool_lit list -> t
val mk_stmt : Proof.step -> Logtk.Statement.input_t -> t
val adapt_f : t -> Proof.form -> t
val adapt_c : t -> SClause.t -> t
val to_llproof : t -> Logtk.LLProof.t
Convert to low level t
val is_proof_of_false : t -> bool
Conversion to a graph of proofs
val as_graph : (t, Proof.rule * Logtk.Subst.t list * Proof.infos) CCGraph.t
Get a graph of the proof
val traverse : ?traversed:unit Tbl.t ->
order:[ `BFS | `DFS ] -> t -> t Sequence.t
IO
val pp_result_of : t CCFormat.printer
val pp_notrec : t CCFormat.printer
Non recursive printing on formatter
val pp_tstp : t CCFormat.printer
val pp_normal : t CCFormat.printer
val pp_zf : t CCFormat.printer
val pp : Logtk.Options.print_format -> t CCFormat.printer
Prints the proof according to the given input switch
val pp_dot : name:string -> t CCFormat.printer
Pretty print the proof as a DOT graph
val pp_dot_file : ?name:string -> string -> t -> unit
print to dot into a file
val pp_dot_seq : name:string -> t Sequence.t CCFormat.printer
Print a set of proofs as a DOT graph, sharing common subproofs
val pp_dot_seq_file : ?name:string -> string -> t Sequence.t -> unit
val step_of_src : Logtk.Statement.Src.t -> Proof.Step.t
val parent_of_sourced : Logtk.Statement.sourced_t -> Proof.Parent.t