Module type Dot.Arg
val print_atom : Stdlib.Format.formatter -> atom -> unit
Print the contents of the given atomic formulas. WARNING: this function should take care to escape and/or not output special reserved characters for the dot format (such as quotes and so on).
val hyp_info : hyp -> string * string option * (Stdlib.Format.formatter -> unit -> unit) list
val lemma_info : lemma -> string * string option * (Stdlib.Format.formatter -> unit -> unit) list
val assumption_info : assumption -> string * string option * (Stdlib.Format.formatter -> unit -> unit) list
Generate some information about the leafs of the proof tree. Currently this backend print each lemma/assumption/hypothesis as a single leaf of the proof tree. These function should return a triplet
(rule, color, l)
, such that:rule
is a name for the proof (arbitrary, does not need to be unique, but should rather be descriptive)color
is a color name (optional) understood by DOTl
is a list of printers that will be called to print some additional information