why3 1.1.1 · OCaml Package

val attrib : 
  string ->
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  'a ->
  unit

val attribs : 
  string ->
  (Format.formatter -> 'a -> unit) ->
  (Format.formatter -> 'b -> unit) ->
  Format.formatter ->
  ('a * 'b) ->
  unit

val empty_elem : 
  string ->
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  'a ->
  unit

val elem : 
  string ->
  (Format.formatter -> 'a -> unit) ->
  (Format.formatter -> 'b -> unit) ->
  Format.formatter ->
  ('a * 'b) ->
  unit

val elem' : 
  string ->
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  'a ->
  unit

val elems : 
  string ->
  (Format.formatter -> 'a -> unit) ->
  'b Pp.pp ->
  Format.formatter ->
  ('a * 'b list) ->
  unit

val elems' : string -> 'a Pp.pp -> Format.formatter -> 'a list -> unit

val pair : 
  (Format.formatter -> 'a -> unit) ->
  (Format.formatter -> 'b -> unit) ->
  Format.formatter ->
  ('a * 'b) ->
  unit

val opt_string_of_bool : bool -> string option

val black_list : string list

val isanitize : string -> string

val fresh_printer : unit -> Ident.ident_printer

val iprinter : Ident.ident_printer

val forget_ids : unit -> unit

val string_of_id : Ident.ident -> string

val tvprinter : Ident.ident_printer

val forget_tvs : unit -> unit

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

val print_vs : Format.formatter -> Term.vsymbol -> unit

val forget_var : Term.vsymbol -> unit

type info = {

}

val print_id : Format.formatter -> Ident.ident -> unit

val print_altname_path : info -> Format.formatter -> Ident.Mid.key -> unit

val print_id_attr : info -> Format.formatter -> Ident.Mid.key -> unit

val print_ts : info -> Format.formatter -> Ty.tysymbol -> unit

val print_ls : info -> Format.formatter -> Term.lsymbol -> unit

val print_pr : info -> Format.formatter -> Decl.prsymbol -> unit

val print_id_real : info -> Format.formatter -> Ident.Mid.key -> unit

val print_ts_real : info -> Format.formatter -> Ty.tysymbol -> unit

val print_ty : info -> Ty.ty Pp.pp

val print_fun_type : 
  info ->
  Format.formatter ->
  (Ty.ty list * Ty.ty option) ->
  unit

val print_ls_type : info -> Format.formatter -> Term.lsymbol -> unit

val print_ls_real : 
  info ->
  Term.Sls.t ->
  Format.formatter ->
  (Term.Sls.elt * (Ty.ty list * Ty.ty option)) ->
  unit

val print_app : 
  (Format.formatter -> 'a -> unit) ->
  'b Pp.pp ->
  Format.formatter ->
  ('a * 'b list) ->
  unit

val print_var : info -> Format.formatter -> Term.vsymbol -> unit

val print_const : Format.formatter -> string -> unit

val print_abs : 
  info ->
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  (Term.vsymbol * 'a) ->
  unit

val p_type : Term.pattern -> Ty.ty

val split_por : Term.pattern -> Term.pattern list

val print_pat : info -> Term.pattern Pp.pp

val binop_name : Term.binop -> string

val print_term : info -> Term.Sls.t -> Term.term Pp.pp

val print_quant : 
  info ->
  Term.Sls.t ->
  string ->
  Format.formatter ->
  (Term.vsymbol list * Term.term) ->
  unit

val print_branch : info -> Term.Sls.t -> Term.term_branch Pp.pp

val dest_conj : Term.term -> Term.term list

val dest_rule : 
  Term.vsymbol list ->
  Term.term list ->
  Term.term ->
  Term.vsymbol list * Term.term list * Term.term

val dest_forall : 
  Term.vsymbol list ->
  Term.term ->
  Term.vsymbol list * Term.term

val print_constr : 
  info ->
  Format.formatter ->
  (Term.lsymbol * Term.lsymbol option list) ->
  unit

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

val print_data_decl : 
  info ->
  Format.formatter ->
  (Ty.tysymbol * (Term.lsymbol * Term.lsymbol option list) list) ->
  unit

val print_data_decls : 
  info ->
  Format.formatter ->
  (Ty.tysymbol * (Term.lsymbol * Term.lsymbol option list) list) list ->
  unit

val print_statement : 
  string ->
  (Format.formatter -> 'a -> unit) ->
  'a ->
  info ->
  Format.formatter ->
  Term.term ->
  unit

val print_equivalence_lemma : 
  info ->
  Format.formatter ->
  (Term.lsymbol * Decl.ls_defn) ->
  unit

val print_fun_eqn : 
  string ->
  info ->
  Term.Sls.t ->
  Format.formatter ->
  (Term.lsymbol * Decl.ls_defn) ->
  unit

val print_logic_decl : 
  info ->
  Format.formatter ->
  (Term.Sls.elt * Decl.ls_defn) ->
  unit

val print_recursive_decl : 
  info ->
  Format.formatter ->
  (Term.Sls.elt * Decl.ls_defn) list ->
  unit

val print_ind : 
  info ->
  Term.Sls.t ->
  Format.formatter ->
  (Decl.prsymbol * Term.term) ->
  unit

val print_ind_decl : 
  info ->
  Term.Sls.t ->
  Format.formatter ->
  (Term.lsymbol * (Decl.prsymbol * Term.term) list) ->
  unit

val print_coind : Format.formatter -> Decl.ind_sign -> unit

val print_ind_decls : 
  info ->
  Decl.ind_sign ->
  Format.formatter ->
  (Term.Sls.elt * (Decl.prsymbol * Term.term) list) list ->
  unit

val print_type_decl : info -> Format.formatter -> Ty.tysymbol -> unit

val print_param_decl : info -> Format.formatter -> Term.lsymbol -> unit

val print_prop_decl : 
  info ->
  Format.formatter ->
  (Decl.prop_kind * Decl.prsymbol * Term.term) ->
  unit

val print_decl : info -> Format.formatter -> Decl.decl -> unit

val print_decls : info -> Format.formatter -> Decl.decl list -> unit

val make_thname : Theory.theory -> string

val print_task : 
  Printer.printer_args ->
  bool ->
  Format.formatter ->
  Task.task ->
  unit

val print_task_full : 
  Printer.printer_args ->
  ?old:'a ->
  Format.formatter ->
  Task.task ->
  unit

val print_task_real : 
  Printer.printer_args ->
  ?old:'a ->
  Format.formatter ->
  Task.task ->
  unit

package why3