package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type pattern =
  1. | PatHole of int
  2. | PatApp of Env.pathname * string * string list * pattern list
val incremental_pat_match : Env.env -> Term.term option array -> pattern -> Term.term -> unit
val pat_match : Env.env -> int -> pattern -> Term.term -> Term.term array
type info = {
  1. info_env : Env.env;
  2. info_symbols : Ident.Sid.t;
  3. info_ops_of_rel : (string * string * string) Term.Mls.t;
  4. info_syn : Printer.syntax_map;
}
val int_minus : Term.lsymbol ref
val real_minus : Term.lsymbol ref
val arith_meta : Theory.meta
val find_th : Env.env -> string -> string -> string -> Term.lsymbol
val get_info : Env.env -> Task.task -> info
val ident_printer : Ident.ident_printer
val print_ident : Format.formatter -> Ident.ident -> unit
val print_const : Format.formatter -> Number.constant -> unit
val constant_value : Term.term -> string
val rel_error_pat : pattern
val print_term : info -> Term.term Pp.pp
val print_fmla : info -> Format.formatter -> Term.term -> unit
exception AlreadyDefined
val is_number : Ty.ty_node -> bool
val filter_logic : info -> ('a * (Term.lsymbol * 'b) list * (Term.lsymbol * 'b) list * 'c) -> (Term.lsymbol * 'b) -> 'a * (Term.lsymbol * 'b) list * (Term.lsymbol * 'b) list * 'c
val filter_hyp : 'a -> Term.lsymbol list -> unit Ident.Hid.t -> ('b * Term.term * Term.term) list -> ('b * Term.term) list -> 'b -> Term.term -> Term.lsymbol list * ('b * Term.term * Term.term) list * ('b * Term.term) list
type filter_goal =
  1. | Goal_good of Decl.prsymbol * Term.term
  2. | Goal_bad of string
  3. | Goal_none
val filter_goal : Decl.prsymbol -> Term.term -> filter_goal
val print_equation : info -> Format.formatter -> (Decl.prsymbol * Term.term * Term.term) -> unit
val print_logic_binder : 'a -> Format.formatter -> Term.vsymbol -> unit
val print_fun_def : info -> Format.formatter -> (Term.lsymbol * Decl.ls_defn) -> unit
val print_pred_def : info -> Format.formatter -> (Term.lsymbol * Decl.ls_defn) -> unit
val print_type_def : 'a -> Format.formatter -> (Ty.tysymbol * 'b list) -> unit
val print_hyp : info -> Format.formatter -> (Decl.prsymbol * Term.term) -> unit
val is_integer : Ty.ty_node -> bool
val print_dom : 'a -> Format.formatter -> Term.lsymbol -> unit
val print_param : 'a -> Format.formatter -> Term.lsymbol -> unit
val print_var : info -> Format.formatter -> Term.vsymbol -> unit
val print_goal : info -> Format.formatter -> filter_goal -> unit
val print_task : Printer.printer_args -> ?old:'a -> Format.formatter -> Task.task -> unit
OCaml

Innovation. Community. Security.