package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
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
OCaml

Innovation. Community. Security.