package why3

  1. Overview
  2. Docs
package why3
Legend:
Library
Module
Module type
Parameter
Class
Class type
val black_list : string list
val fresh_printer : unit -> Ident.ident_printer
val iprinter : Ident.ident_printer
val forget_all : unit -> unit
val tv_set : Ident.Sid.t Stdlib.ref
val thprinter : Ident.ident_printer
val print_tv : Stdlib.Format.formatter -> Ty.tvsymbol -> unit
val print_tv_binder : Stdlib.Format.formatter -> Ty.tvsymbol -> unit
val print_params_list : Stdlib.Format.formatter -> Ty.tvsymbol list -> unit
val print_params : Stdlib.Format.formatter -> Ty.Stv.t -> unit
val forget_tvs : unit -> unit
val print_vs : Stdlib.Format.formatter -> Term.vsymbol -> unit
val forget_var : Term.vsymbol -> unit
val print_ts : Stdlib.Format.formatter -> Ty.tysymbol -> unit
val print_ls : Stdlib.Format.formatter -> Term.lsymbol -> unit
val print_pr : Stdlib.Format.formatter -> Decl.prsymbol -> unit
val print_name : Stdlib.Format.formatter -> Ident.ident -> unit
val get_th_name : Ident.ident -> string
type info = {
  1. info_syn : Printer.syntax_map;
  2. symbol_printers : (string * Theory.theory * Ident.ident_printer) Ident.Mid.t;
  3. realization : bool;
}
val print_path : string list Pp.pp
val print_id : Stdlib.Format.formatter -> Ident.ident -> unit
val print_id_real : info -> Stdlib.Format.formatter -> Ident.Mid.key -> unit
val print_ls_real : info -> Stdlib.Format.formatter -> Term.lsymbol -> unit
val print_ts_real : info -> Stdlib.Format.formatter -> Ty.tysymbol -> unit
val print_pr_real : info -> Stdlib.Format.formatter -> Decl.prsymbol -> unit
val print_ty : info -> Ty.ty Pp.pp
val unambig_fs : Term.lsymbol -> bool
val lparen_l : Stdlib.Format.formatter -> unit -> unit
val lparen_r : Stdlib.Format.formatter -> unit -> unit
val print_paren_l : 'a Pp.pp -> Stdlib.Format.formatter -> 'a list -> unit
val print_paren_r : 'a Pp.pp -> Stdlib.Format.formatter -> 'a list -> unit
val arrow : Stdlib.Format.formatter -> unit -> unit
val print_arrow_list : 'a Pp.pp -> Stdlib.Format.formatter -> 'a list -> unit
val print_space_list : 'a Pp.pp -> Stdlib.Format.formatter -> 'a list -> unit
val print_comma_list : 'a Pp.pp -> Stdlib.Format.formatter -> 'a list -> unit
val print_or_list : 'a Pp.pp -> Stdlib.Format.formatter -> 'a list -> unit
val comma_newline : Stdlib.Format.formatter -> unit -> unit
val print_pat : info -> Term.pattern Pp.pp
val print_vsty_nopar : info -> Stdlib.Format.formatter -> Term.vsymbol -> unit
val print_vsty : info -> Stdlib.Format.formatter -> Term.vsymbol -> unit
val is_tuple0_ty : Ty.ty option -> bool
val is_tuple_ty : Ty.ty option -> bool
val print_binop : Stdlib.Format.formatter -> Term.binop -> unit
val print_attr : 'a -> ('b * 'c) -> unit
val protect_on : bool -> ('a, 'b, 'c, 'd, 'e, 'f) Stdlib.format6 -> ('a, 'b, 'c, 'd, 'e, 'f) Stdlib.format6
val number_format : Number.number_support
val print_term : info -> Term.term Pp.pp
val print_fmla : info -> Term.term Pp.pp
val print_opl_term : info -> Stdlib.Format.formatter -> Term.term -> unit
val print_opl_fmla : info -> Stdlib.Format.formatter -> Term.term -> unit
val print_opr_term : info -> Stdlib.Format.formatter -> Term.term -> unit
val print_opr_fmla : info -> Stdlib.Format.formatter -> Term.term -> unit
val print_lrterm : bool -> bool -> info -> Stdlib.Format.formatter -> Term.term -> unit
val print_lrfmla : bool -> bool -> info -> Stdlib.Format.formatter -> Term.term -> unit
val print_tnode : bool -> bool -> info -> Stdlib.Format.formatter -> Term.term -> unit
val print_fnode : bool -> bool -> info -> Stdlib.Format.formatter -> Term.term -> unit
val print_tuple_pat : info -> Term.term -> Stdlib.Format.formatter -> Term.pattern -> unit
val print_branch : (info -> Stdlib.Format.formatter -> Term.term -> unit) -> info -> Stdlib.Format.formatter -> Term.term_branch -> unit
val print_branches : ?first:bool -> (info -> Term.term Pp.pp) -> info -> Stdlib.Format.formatter -> Term.term_branch list -> unit
val print_expr : info -> Stdlib.Format.formatter -> Term.term -> unit
val print_constr : info -> 'a -> Stdlib.Format.formatter -> (Term.lsymbol * 'b) -> unit
val ls_ty_vars : Term.lsymbol -> Ty.Stv.t * Ty.Stv.t * Ty.Stv.t
val clean_line : string -> string
type contents = string list
type chunk =
  1. | Edition of string * contents
  2. | Other of contents
val re_blank : Re.Str.regexp
val re_why3 : Re.Str.regexp
val read_old_script : Stdlib.in_channel -> chunk list
val print_contents : Stdlib.Format.formatter -> string list -> unit
val output_till_statement : Stdlib.Format.formatter -> chunk list Stdlib.ref -> string -> chunk option
val print_contents_in_comment : Stdlib.Format.formatter -> string list -> unit
val output_remaining : Stdlib.Format.formatter -> chunk list -> unit
val print_user_def : Stdlib.Format.formatter -> string list -> unit
val realization : Stdlib.Format.formatter -> info -> chunk option -> unit
val print_type_decl : prev:chunk option -> info -> Stdlib.Format.formatter -> Ty.tysymbol -> unit
val print_data_decl : info -> Stdlib.Format.formatter -> (Ty.tysymbol * (Term.lsymbol * 'a) list) -> unit
val print_ls_type : info -> Stdlib.Format.formatter -> Ty.ty option -> unit
val create_argument : Ty.ty -> Term.vsymbol
val print_arguments : info -> Stdlib.Format.formatter -> Term.vsymbol list -> unit
val re_macro : Re.Str.regexp
val has_macro : string -> bool
val is_macro : info -> Stdlib.Format.formatter -> chunk option -> unit
val print_param_decl : prev:chunk option -> info -> Stdlib.Format.formatter -> Term.lsymbol -> unit
val print_logic_decl : prev:'a -> info -> Stdlib.Format.formatter -> (Term.lsymbol * Decl.ls_defn) -> unit
val print_recursive_decl : info -> Stdlib.Format.formatter -> (Term.lsymbol * Decl.ls_defn) -> unit
val print_ind : info -> Stdlib.Format.formatter -> (Decl.prsymbol * Term.term) -> unit
val print_ind_decl : info -> Stdlib.Format.formatter -> (Term.lsymbol * ('a * Term.term) list) -> unit
val re_lemma : Re.Str.regexp
val find_lemma : string list -> string
val axiom_or_lemma : chunk option -> string
val print_prop_decl : prev:'a -> info -> Stdlib.Format.formatter -> (Decl.prop_kind * Decl.prsymbol * Term.term) -> unit
val print_decl : old:chunk list Stdlib.ref -> info -> Stdlib.Format.formatter -> Decl.decl -> unit
val print_decls : old:chunk list Stdlib.ref -> info -> Stdlib.Format.formatter -> Decl.decl list -> unit
val init_printer : Theory.theory -> Ident.ident_printer
val print_task : Printer.printer_args -> bool -> ?old:Stdlib.in_channel -> Stdlib.Format.formatter -> Task.task -> unit
val print_task_full : Printer.printer_args -> ?old:Stdlib.in_channel -> Stdlib.Format.formatter -> Task.task -> unit
val print_task_real : Printer.printer_args -> ?old:Stdlib.in_channel -> 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