package why3

  1. Overview
  2. Docs
package why3
Legend:
Library
Module
Module type
Parameter
Class
Class type
val attrib : string -> (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a -> unit
val attribs : string -> (Stdlib.Format.formatter -> 'a -> unit) -> (Stdlib.Format.formatter -> 'b -> unit) -> Stdlib.Format.formatter -> ('a * 'b) -> unit
val empty_elem : string -> (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a -> unit
val elem : string -> (Stdlib.Format.formatter -> 'a -> unit) -> (Stdlib.Format.formatter -> 'b -> unit) -> Stdlib.Format.formatter -> ('a * 'b) -> unit
val elem' : string -> (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a -> unit
val elems : string -> (Stdlib.Format.formatter -> 'a -> unit) -> 'b Pp.pp -> Stdlib.Format.formatter -> ('a * 'b list) -> unit
val elems' : string -> 'a Pp.pp -> Stdlib.Format.formatter -> 'a list -> unit
val pair : (Stdlib.Format.formatter -> 'a -> unit) -> (Stdlib.Format.formatter -> 'b -> unit) -> Stdlib.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 : Stdlib.Format.formatter -> Ty.tvsymbol -> unit
val print_vs : Stdlib.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 : Stdlib.Format.formatter -> Ident.ident -> unit
val print_altname_path : info -> Stdlib.Format.formatter -> Ident.Mid.key -> unit
val print_id_attr : info -> Stdlib.Format.formatter -> Ident.Mid.key -> unit
val print_ts : info -> Stdlib.Format.formatter -> Ty.tysymbol -> unit
val print_ls : info -> Stdlib.Format.formatter -> Term.lsymbol -> unit
val print_pr : info -> Stdlib.Format.formatter -> Decl.prsymbol -> unit
val print_id_real : info -> Stdlib.Format.formatter -> Ident.Mid.key -> unit
val print_ts_real : info -> Stdlib.Format.formatter -> Ty.tysymbol -> unit
val print_ty : info -> Ty.ty Pp.pp
val print_fun_type : info -> Stdlib.Format.formatter -> (Ty.ty list * Ty.ty option) -> unit
val print_ls_type : info -> Stdlib.Format.formatter -> Term.lsymbol -> unit
val print_ls_real : info -> Term.Sls.t -> Stdlib.Format.formatter -> (Term.Sls.elt * (Ty.ty list * Ty.ty option)) -> unit
val print_app : (Stdlib.Format.formatter -> 'a -> unit) -> 'b Pp.pp -> Stdlib.Format.formatter -> ('a * 'b list) -> unit
val print_var : info -> Stdlib.Format.formatter -> Term.vsymbol -> unit
val print_const : Stdlib.Format.formatter -> string -> unit
val print_abs : info -> (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.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 number_format : (Stdlib.Format.formatter -> unit) -> Number.number_support
val print_term : info -> Term.Sls.t -> Term.term Pp.pp
val print_quant : info -> Term.Sls.t -> string -> Stdlib.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 -> Stdlib.Format.formatter -> (Term.lsymbol * Term.lsymbol option list) -> unit
val print_tparams : Stdlib.Format.formatter -> Ty.tvsymbol list -> unit
val print_data_decl : info -> Stdlib.Format.formatter -> (Ty.tysymbol * (Term.lsymbol * Term.lsymbol option list) list) -> unit
val print_data_decls : info -> Stdlib.Format.formatter -> (Ty.tysymbol * (Term.lsymbol * Term.lsymbol option list) list) list -> unit
val print_statement : string -> (Stdlib.Format.formatter -> 'a -> unit) -> 'a -> info -> Stdlib.Format.formatter -> Term.term -> unit
val print_equivalence_lemma : info -> Stdlib.Format.formatter -> (Term.lsymbol * Decl.ls_defn) -> unit
val print_fun_eqn : string -> info -> Term.Sls.t -> Stdlib.Format.formatter -> (Term.lsymbol * Decl.ls_defn) -> unit
val print_logic_decl : info -> Stdlib.Format.formatter -> (Term.Sls.elt * Decl.ls_defn) -> unit
val print_recursive_decl : info -> Stdlib.Format.formatter -> (Term.Sls.elt * Decl.ls_defn) list -> unit
val print_ind : info -> Term.Sls.t -> Stdlib.Format.formatter -> (Decl.prsymbol * Term.term) -> unit
val print_ind_decl : info -> Term.Sls.t -> Stdlib.Format.formatter -> (Term.lsymbol * (Decl.prsymbol * Term.term) list) -> unit
val print_coind : Stdlib.Format.formatter -> Decl.ind_sign -> unit
val print_ind_decls : info -> Decl.ind_sign -> Stdlib.Format.formatter -> (Term.Sls.elt * (Decl.prsymbol * Term.term) list) list -> unit
val print_type_decl : info -> Stdlib.Format.formatter -> Ty.tysymbol -> unit
val print_param_decl : info -> Stdlib.Format.formatter -> Term.lsymbol -> unit
val print_prop_decl : info -> Stdlib.Format.formatter -> (Decl.prop_kind * Decl.prsymbol * Term.term) -> unit
val print_decl : info -> Stdlib.Format.formatter -> Decl.decl -> unit
val print_decls : info -> Stdlib.Format.formatter -> Decl.decl list -> unit
val make_thname : Theory.theory -> string
val print_task : Printer.printer_args -> bool -> Stdlib.Format.formatter -> Task.task -> unit
val print_task_full : Printer.printer_args -> ?old:'a -> Stdlib.Format.formatter -> Task.task -> unit
val print_task_real : Printer.printer_args -> ?old:'a -> Stdlib.Format.formatter -> Task.task -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct