Module type Pretty.Printer

module type Printer = sig .. end

val tprinter : Why3.Ident.ident_printer

printer for identifiers of type symbols

val aprinter : Why3.Ident.ident_printer

printer for identifiers of type variables

val sprinter : Why3.Ident.ident_printer

printer for identifiers of variables and functions

val pprinter : Why3.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 : Why3.Term.vsymbol -> unit

flush id_unique for a variable

val print_id_attrs : Why3.Ident.ident Why3.Pp.pp

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

val print_tv : Why3.Ty.tvsymbol Why3.Pp.pp

val print_vs : Why3.Term.vsymbol Why3.Pp.pp

val print_ts : Why3.Ty.tysymbol Why3.Pp.pp

val print_ls : Why3.Term.lsymbol Why3.Pp.pp

val print_cs : Why3.Term.lsymbol Why3.Pp.pp

val print_pr : Why3.Decl.prsymbol Why3.Pp.pp

val print_th : Why3.Theory.theory Why3.Pp.pp

val print_ty : Why3.Ty.ty Why3.Pp.pp

val print_vsty : Why3.Term.vsymbol Why3.Pp.pp

prints ``variable : type''

val print_ts_qualified : Why3.Ty.tysymbol Why3.Pp.pp

val print_ls_qualified : Why3.Term.lsymbol Why3.Pp.pp

val print_cs_qualified : Why3.Term.lsymbol Why3.Pp.pp

val print_pr_qualified : Why3.Decl.prsymbol Why3.Pp.pp

val print_th_qualified : Why3.Theory.theory Why3.Pp.pp

val print_ty_qualified : Why3.Ty.ty Why3.Pp.pp

val print_vs_qualified : Why3.Term.vsymbol Why3.Pp.pp

val print_tv_qualified : Why3.Ty.tvsymbol Why3.Pp.pp

val print_quant : Why3.Term.quant Why3.Pp.pp

val print_binop : asym:bool -> Why3.Term.binop Why3.Pp.pp

val print_pat : Why3.Term.pattern Why3.Pp.pp

val print_term : Why3.Term.term Why3.Pp.pp

val print_attr : Why3.Ident.attribute Why3.Pp.pp

val print_attrs : Why3.Ident.Sattr.t Why3.Pp.pp

val print_loc_as_attribute : Why3.Loc.position Why3.Pp.pp

val print_pkind : Why3.Decl.prop_kind Why3.Pp.pp

val print_meta_arg : Why3.Theory.meta_arg Why3.Pp.pp

val print_meta_arg_type : Why3.Theory.meta_arg_type Why3.Pp.pp

val print_ty_decl : Why3.Ty.tysymbol Why3.Pp.pp

val print_data_decl : Why3.Decl.data_decl Why3.Pp.pp

val print_param_decl : Why3.Term.lsymbol Why3.Pp.pp

val print_logic_decl : Why3.Decl.logic_decl Why3.Pp.pp

val print_ind_decl : Why3.Decl.ind_sign -> Why3.Decl.ind_decl Why3.Pp.pp

val print_next_data_decl : Why3.Decl.data_decl Why3.Pp.pp

val print_next_logic_decl : Why3.Decl.logic_decl Why3.Pp.pp

val print_next_ind_decl : Why3.Decl.ind_decl Why3.Pp.pp

val print_prop_decl : Why3.Decl.prop_decl Why3.Pp.pp

val print_decl : Why3.Decl.decl Why3.Pp.pp

val print_tdecl : Why3.Theory.tdecl Why3.Pp.pp

val print_task : Why3.Task.task Why3.Pp.pp

val print_sequent : Why3.Task.task Why3.Pp.pp

val print_theory : Why3.Theory.theory Why3.Pp.pp

val print_namespace : string -> Why3.Theory.theory Why3.Pp.pp