why3 1.3.2 · OCaml Package

val sml_remove : Ident.attribute

val is_sml_remove : attrs:Ident.Sattr.t -> bool

val iprinter : Ident.ident_printer

val aprinter : Ident.ident_printer

val tprinter : Ident.ident_printer

val forget_id : Ident.ident -> unit

val _forget_ids : Ident.ident list -> unit

val forget_var : Mltree.var -> unit

val forget_vars : Mltree.var list -> unit

val forget_let_defn : Mltree.let_def -> unit

val forget_pat : Mltree.pat -> unit

val print_global_ident : 
  sanitizer:(string -> string) ->
  Format.formatter ->
  Ident.ident ->
  unit

val print_path : 
  sanitizer:(string -> string) ->
  Format.formatter ->
  (string list * Ident.ident) ->
  unit

val print_lident : Ml_printer.info -> Format.formatter -> Ident.Sid.elt -> unit

val print_uident : Ml_printer.info -> Format.formatter -> Ident.Sid.elt -> unit

val print_tv : Format.formatter -> Ty.tvsymbol -> unit

val print_rs : Ml_printer.info -> Format.formatter -> Expr.rsymbol -> unit

val check_type_in_drv : Ml_printer.info -> Ident.ident -> unit

val print_ty : ?paren:bool -> Ml_printer.info -> Mltree.ty Pp.pp

val print_vsty : 
  Ml_printer.info ->
  Format.formatter ->
  (Ident.Sid.elt * 'a * 'b) ->
  unit

val print_tv_arg : Format.formatter -> Ty.tvsymbol -> unit

val print_tv_args : Format.formatter -> Ty.tvsymbol list -> unit

val print_vs_arg : 
  Ml_printer.info ->
  Format.formatter ->
  (Ident.Sid.elt * 'a * 'b) ->
  unit

val get_record : Ml_printer.info -> Expr.rsymbol -> Expr.rsymbol list

val print_pat : Ml_printer.info -> Mltree.pat Pp.pp

val print_papp : 
  Ml_printer.info ->
  Term.lsymbol ->
  Format.formatter ->
  Mltree.pat list ->
  unit

val pv_name : Ity.pvsymbol -> Ident.ident

val print_pv : Ml_printer.info -> Format.formatter -> Ity.pvsymbol -> unit

val is_true : Mltree.expr -> bool

val is_false : Mltree.expr -> bool

val is_mapped_to_int : Ml_printer.info -> Ity.ity -> bool

val escape : char -> string

val print_constant : Format.formatter -> Mltree.expr -> unit

val print_for_direction : Format.formatter -> Mltree.for_direction -> unit

val print_apply_args : 
  Ml_printer.info ->
  Format.formatter ->
  (Mltree.expr list * Ity.pvsymbol list) ->
  unit

val print_apply : 
  Ml_printer.info ->
  Expr.rsymbol ->
  Format.formatter ->
  Mltree.expr list ->
  unit

val print_svar : Format.formatter -> Ty.Stv.t -> unit

val print_fun_type_args : 
  Ml_printer.info ->
  Format.formatter ->
  (Mltree.var list * Ty.Stv.t * Mltree.ty * Mltree.expr) ->
  unit

val print_let_def : 
  Ml_printer.info ->
  Format.formatter ->
  Mltree.let_def ->
  unit

val print_expr : ?paren:bool -> Ml_printer.info -> Mltree.expr Pp.pp

val print_branch : Ml_printer.info -> bool -> Mltree.reg_branch Pp.pp

val print_raise : 
  paren:bool ->
  Ml_printer.info ->
  Ity.xsymbol ->
  Format.formatter ->
  Mltree.expr option ->
  unit

val print_xbranch : bool -> Ml_printer.info -> bool -> Mltree.exn_branch Pp.pp

val print_type_decl : 
  Ml_printer.info ->
  Format.formatter ->
  Mltree.its_defn ->
  unit

val extract_module_decl : Mltree.decl list -> Mltree.decl list

val print_decl : Ml_printer.info -> Format.formatter -> Mltree.decl -> unit

package why3