module ProofPrint: sig .. end
Manipulate proofs
type ProofStep.of_
val is_proof_of_false : t -> bool
Conversion to a graph of proofs
module Tbl: module type of ProofStep.PTbl
val as_graph : (t, t * ProofStep.rule * t) CCGraph.t
Get a graph of the proof
val traverse : ?traversed:unit Tbl.t -> t -> t Sequence.t
IO
val pp_result : ProofStep.result CCFormat.printer
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 : Libzipperposition.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