why3 1.1.1 · OCaml Package

why3

val coercion_attr : Ident.attribute

val why3_keywords : string list

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

val create : 
  Ident.ident_printer ->
  Ident.ident_printer ->
  Ident.ident_printer ->
  Ident.ident_printer ->
  bool ->
  (module Printer)

package why3