package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 = {
  1. info_syn : Printer.syntax_map;
  2. symbol_printers : (string * Ident.ident_printer) Ident.Mid.t;
  3. realization : bool;
  4. theories : string Ident.Mid.t;
}
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
OCaml

Innovation. Community. Security.