Module Proof.S

type t = proof
val result : t -> result
val step : t -> 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

Constructors and utils

In all the following constructors, theories defaults to the empty list. Axiom constructors have default role "axiom"

val mk : step -> Result.t -> t

Main constructor

val mk_f : step -> form -> t
val mk_f_trivial : form -> t
val mk_f_by_def : ID.t -> form -> t
val mk_f_inference : rule:rule -> form -> parent list -> t
val mk_f_simp : rule:rule -> form -> parent list -> t
val mk_f_esa : rule:rule -> form -> parent list -> t
val name : namespace:string Tbl.t -> t -> string
val adapt : t -> Result.t -> t
val adapt_f : t -> form -> t
val is_proof_of_false : t -> bool
Conversion to a graph of proofs
val as_graph : (t, rule * Subst.Projection.t option * infos) CCGraph.t

Get a graph of the proof

val traverse : ?traversed:unit Tbl.t -> order:[ `BFS | `DFS ] -> t -> t Iter.t
IO
val pp_result_of : t CCFormat.printer
val pp_notrec : t CCFormat.printer

Non recursive printing on formatter

val pp_notrec1 : t CCFormat.printer

Non recursive printing on formatter, including parents

val pp_tstp : t CCFormat.printer
val pp_normal : t CCFormat.printer
val pp_zf : 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 Iter.t CCFormat.printer

Print a set of proofs as a DOT graph, sharing common subproofs

val pp_dot_seq_file : ?name:string -> string -> t Iter.t -> unit

same as pp_dot_seq but into a file