Module type Pretty.Printer

module type Printer = sig .. end

val tprinter : Ident.ident_printer

printer for identifiers of type symbols

val aprinter : Ident.ident_printer

printer for identifiers of type variables

val sprinter : Ident.ident_printer

printer for identifiers of variables and functions

val pprinter : Ident.ident_printer

printer for identifiers of proposition

val forget_all : unit -> unit

flush id_unique

val forget_tvs : unit -> unit

flush id_unique for type vars

val forget_var : Term.vsymbol -> unit

flush id_unique for a variable

val print_id_attrs : Ident.ident Pp.pp

prints attributes and location of an ident (but not the ident itself)

val print_tv : Ty.tvsymbol Pp.pp
val print_vs : Term.vsymbol Pp.pp
val print_ts : Ty.tysymbol Pp.pp
val print_ls : Term.lsymbol Pp.pp
val print_cs : Term.lsymbol Pp.pp
val print_pr : Decl.prsymbol Pp.pp
val print_th : Theory.theory Pp.pp
val print_ty : Ty.ty Pp.pp
val print_vsty : Term.vsymbol Pp.pp

prints ``variable : type''

val print_ts_qualified : Ty.tysymbol Pp.pp
val print_ls_qualified : Term.lsymbol Pp.pp
val print_cs_qualified : Term.lsymbol Pp.pp
val print_pr_qualified : Decl.prsymbol Pp.pp
val print_th_qualified : Theory.theory Pp.pp
val print_ty_qualified : Ty.ty Pp.pp
val print_vs_qualified : Term.vsymbol Pp.pp
val print_tv_qualified : Ty.tvsymbol Pp.pp
val print_quant : Term.quant Pp.pp
val print_binop : asym:bool -> Term.binop Pp.pp
val print_pat : Term.pattern Pp.pp
val print_term : Term.term Pp.pp
val print_attr : Ident.attribute Pp.pp
val print_attrs : Ident.Sattr.t Pp.pp
val print_loc_as_attribute : Loc.position Pp.pp
val print_pkind : Decl.prop_kind Pp.pp
val print_meta_arg : Theory.meta_arg Pp.pp
val print_meta_arg_type : Theory.meta_arg_type Pp.pp
val print_ty_decl : Ty.tysymbol Pp.pp
val print_data_decl : Decl.data_decl Pp.pp
val print_param_decl : Term.lsymbol Pp.pp
val print_logic_decl : Decl.logic_decl Pp.pp
val print_ind_decl : Decl.ind_sign -> Decl.ind_decl Pp.pp
val print_next_data_decl : Decl.data_decl Pp.pp
val print_next_logic_decl : Decl.logic_decl Pp.pp
val print_next_ind_decl : Decl.ind_decl Pp.pp
val print_prop_decl : Decl.prop_decl Pp.pp
val print_decl : Decl.decl Pp.pp
val print_tdecl : Theory.tdecl Pp.pp
val print_task : Task.task Pp.pp
val print_sequent : Task.task Pp.pp
val print_theory : Theory.theory Pp.pp
val print_namespace : string -> Theory.theory Pp.pp