Module `Dot.Simple`

Functor for making a module to export proofs to the DOT format. The substitution of the hyp type is non-destructive due to a restriction of destructive substitutions on earlier versions of ocaml.

Parameters

S : Msat.S
A : Arg with type atom := S.formula and type hyp = S.formula list and type lemma := S.lemma and type assumption = S.formula

Signature

type t: The type of proofs.

val pp : Format.formatter -> t -> unit: A function for printing proofs in the desired format.