why3 1.3.2 · OCaml Package

val coercion_attr : Ident.attribute

val why3_keywords : string list

val prio_binop : Term.binop -> int

val protect_on : 
  bool ->
  ('a, 'b, 'c, 'd, 'e, 'f) format6 ->
  ('a, 'b, 'c, 'd, 'e, 'f) format6

type syntax =

| Is_array of string
| Is_getter of string
| Is_none

val get_element_syntax : attrs:Ident.Sattr.t -> syntax

module type Printer = sig ... end

val tprinter : Ident.ident_printer

val aprinter : Ident.ident_printer

val sprinter : Ident.ident_printer

val pprinter : Ident.ident_printer

val forget_all : unit -> unit

val forget_tvs : unit -> unit

val forget_var : Term.vsymbol -> unit

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

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

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

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

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

val print_cs : Format.formatter -> Term.lsymbol -> unit

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

val print_th : Format.formatter -> Theory.theory -> unit

val print_ty : Format.formatter -> Ty.ty -> unit

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

val print_ts_qualified : Format.formatter -> Ty.tysymbol -> unit

val print_ls_qualified : Format.formatter -> Term.lsymbol -> unit

val print_cs_qualified : Format.formatter -> Term.lsymbol -> unit

val print_pr_qualified : Format.formatter -> Decl.prsymbol -> unit

val print_th_qualified : Format.formatter -> Theory.theory -> unit

val print_ty_qualified : Format.formatter -> Ty.ty -> unit

val print_quant : Format.formatter -> Term.quant -> unit

val print_binop : asym:bool -> Format.formatter -> Term.binop -> unit

val print_pat : Format.formatter -> Term.pattern -> unit

val print_term : Format.formatter -> Term.term -> unit

val print_attr : Format.formatter -> Ident.attribute -> unit

val print_loc : Format.formatter -> Loc.position -> unit

val print_pkind : Format.formatter -> Decl.prop_kind -> unit

val print_meta_arg : Format.formatter -> Theory.meta_arg -> unit

val print_meta_arg_type : Format.formatter -> Theory.meta_arg_type -> unit

val print_ty_decl : Format.formatter -> Ty.tysymbol -> unit

val print_data_decl : Format.formatter -> Decl.data_decl -> unit

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

val print_logic_decl : Format.formatter -> Decl.logic_decl -> unit

val print_ind_decl : Format.formatter -> Decl.ind_sign -> Decl.ind_decl -> unit

val print_next_data_decl : Format.formatter -> Decl.data_decl -> unit

val print_next_logic_decl : Format.formatter -> Decl.logic_decl -> unit

val print_next_ind_decl : Format.formatter -> Decl.ind_decl -> unit

val print_prop_decl : Format.formatter -> Decl.prop_decl -> unit

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

val print_tdecl : Format.formatter -> Theory.tdecl -> unit

val print_task : Format.formatter -> Task.task -> unit

val print_sequent : Format.formatter -> Task.task -> unit

val print_theory : Format.formatter -> Theory.theory -> unit

val print_namespace : Format.formatter -> string -> Theory.theory -> unit

type any_pp =

| Pp_term of Term.term * int
| Pp_ty of Ty.ty * int * bool
| Pp_decl of bool * Ty.tysymbol * (Term.lsymbol * Term.lsymbol option list) list
| Pp_ts of Ty.tysymbol
| Pp_ls of Term.lsymbol
| Pp_id of Ident.ident
| Pp_cs of Term.lsymbol
| Pp_vs of Term.vsymbol
| Pp_trigger of Term.trigger
| Pp_forget of Term.vsymbol list
| Pp_forget_tvs

val create : 
  ?print_ext_any:(any_pp Pp.pp -> any_pp Pp.pp) ->
  Ident.ident_printer ->
  Ident.ident_printer ->
  Ident.ident_printer ->
  Ident.ident_printer ->
  bool ->
  (module Printer)

package why3