package why3

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

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