To focus the search input from anywhere on the page, press the 'S' key.
in-package search v0.1.0
Library
Module
Module type
Parameter
Class
Class type
Provides a reasonnable default to instantiate the Make
functor, assuming the original printing functions are compatible with DOT html labels.
Term printing for DOT
This module defines what functions are required in order to export a proof to the DOT format.
Parameters
Signature
val print_atom : Format.formatter -> S.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 :
S.clause ->
string * string option * (Format.formatter -> unit -> unit) list
val lemma_info :
S.clause ->
string * string option * (Format.formatter -> unit -> unit) list
val assumption_info :
S.clause ->
string * string option * (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