package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
exception Unsupported of string
val current_decl_name : string ref
module C : sig ... end
type info = {
  1. env : Env.env;
  2. prelude : Printer.prelude;
  3. thprelude : Printer.prelude_map;
  4. thinterface : Printer.interface_map;
  5. blacklist : Printer.blacklist;
  6. syntax : Printer.syntax_map;
  7. literal : Printer.syntax_map;
  8. kn : Pdecl.known_map;
  9. prec : int list Ident.Mid.t;
}
val debug_c_extraction : Debug.flag
val debug_c_no_error_msgs : Debug.flag
module Print : sig ... end
module MLToC : sig ... end
val name_gen : string -> ?fname:string -> Pmodule.pmodule -> string
val header_border_printer : bool -> 'a -> ?old:'b -> ?fname:string -> flat:'c -> Format.formatter -> Pmodule.pmodule -> unit
val print_header_decl : Pdriver.printer_args -> ?old:in_channel -> ?fname:string -> flat:bool -> Pmodule.pmodule -> Format.formatter -> Mltree.decl -> unit
val print_prelude : 'a -> ?old:'b -> ?fname:'c -> flat:'d -> Pmodule.pmodule list -> Format.formatter -> 'e -> unit
val print_decl : Pdriver.printer_args -> ?old:in_channel -> ?fname:string -> flat:bool -> Pmodule.pmodule -> Format.formatter -> Mltree.decl -> unit
val c_printer : Pdriver.printer
OCaml

Innovation. Community. Security.