Module ConstraintPrettyPrinter (.ml)

module ConstraintPrettyPrinter: sig .. end

The constraint over equality between terms.

type formula = (MultiEquation.crterm, MultiEquation.variable) Constraint.type_constraint

The constraint over equality between terms.

val printf_constraint : ?forall:string ->
       ?exists:string ->
       ?andsym:string ->
       ?before:(formula -> 'a) ->
       ?after:(formula -> 'b) ->
       ?user_name_from_int:(int -> string) ->
       PrettyPrinter.mode -> formula -> unit

Pretty printer for formula. The connectors' representations can be redefined (labels forall, exists, andsym). A user_name_from_int function can be given to generate fresh strings from integers. See PrettyPrinter.mode.