package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val sml_remove : Ident.attribute
val is_sml_remove : attrs:Ident.Sattr.t -> bool
val iprinter : Ident.ident_printer
val aprinter : Ident.ident_printer
val tprinter : Ident.ident_printer
val forget_id : Ident.ident -> unit
val _forget_ids : Ident.ident list -> unit
val forget_var : Mltree.var -> unit
val forget_vars : Mltree.var list -> unit
val forget_let_defn : Mltree.let_def -> unit
val forget_pat : Mltree.pat -> unit
val print_global_ident : sanitizer:(string -> string) -> Format.formatter -> Ident.ident -> unit
val print_path : sanitizer:(string -> string) -> Format.formatter -> (string list * Ident.ident) -> unit
val print_lident : Ml_printer.info -> Format.formatter -> Ident.Sid.elt -> unit
val print_uident : Ml_printer.info -> Format.formatter -> Ident.Sid.elt -> unit
val print_tv : Format.formatter -> Ty.tvsymbol -> unit
val print_rs : Ml_printer.info -> Format.formatter -> Expr.rsymbol -> unit
val check_type_in_drv : Ml_printer.info -> Ident.ident -> unit
val print_ty : ?paren:bool -> Ml_printer.info -> Mltree.ty Pp.pp
val print_vsty : Ml_printer.info -> Format.formatter -> (Ident.Sid.elt * 'a * 'b) -> unit
val print_tv_arg : Format.formatter -> Ty.tvsymbol -> unit
val print_tv_args : Format.formatter -> Ty.tvsymbol list -> unit
val print_vs_arg : Ml_printer.info -> Format.formatter -> (Ident.Sid.elt * 'a * 'b) -> unit
val get_record : Ml_printer.info -> Expr.rsymbol -> Expr.rsymbol list
val print_pat : Ml_printer.info -> Mltree.pat Pp.pp
val print_papp : Ml_printer.info -> Term.lsymbol -> Format.formatter -> Mltree.pat list -> unit
val pv_name : Ity.pvsymbol -> Ident.ident
val print_pv : Ml_printer.info -> Format.formatter -> Ity.pvsymbol -> unit
val is_true : Mltree.expr -> bool
val is_false : Mltree.expr -> bool
val is_mapped_to_int : Ml_printer.info -> Ity.ity -> bool
val escape : char -> string
val print_constant : Format.formatter -> Mltree.expr -> unit
val print_for_direction : Format.formatter -> Mltree.for_direction -> unit
val print_apply_args : Ml_printer.info -> Format.formatter -> (Mltree.expr list * Ity.pvsymbol list) -> unit
val print_apply : Ml_printer.info -> Expr.rsymbol -> Format.formatter -> Mltree.expr list -> unit
val print_svar : Format.formatter -> Ty.Stv.t -> unit
val print_fun_type_args : Ml_printer.info -> Format.formatter -> (Mltree.var list * Ty.Stv.t * Mltree.ty * Mltree.expr) -> unit
val print_let_def : Ml_printer.info -> Format.formatter -> Mltree.let_def -> unit
val print_expr : ?paren:bool -> Ml_printer.info -> Mltree.expr Pp.pp
val print_branch : Ml_printer.info -> bool -> Mltree.reg_branch Pp.pp
val print_raise : paren:bool -> Ml_printer.info -> Ity.xsymbol -> Format.formatter -> Mltree.expr option -> unit
val print_xbranch : bool -> Ml_printer.info -> bool -> Mltree.exn_branch Pp.pp
val print_type_decl : Ml_printer.info -> Format.formatter -> Mltree.its_defn -> unit
val extract_module_decl : Mltree.decl list -> Mltree.decl list
val print_decl : Ml_printer.info -> Format.formatter -> Mltree.decl -> unit
OCaml

Innovation. Community. Security.