package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type prog_symbol =
  1. | PV of Ity.pvsymbol
  2. | RS of Expr.rsymbol
  3. | OO of Expr.Srs.t
val ns_find_prog_symbol : namespace -> string list -> prog_symbol
val ns_find_its : namespace -> string list -> Ity.itysymbol
val ns_find_pv : namespace -> string list -> Ity.pvsymbol
val ns_find_xs : namespace -> string list -> Ity.xsymbol
val ns_find_ns : namespace -> string list -> namespace
val ns_find_rs : namespace -> string list -> Expr.rsymbol
type overload =
  1. | FixedRes of Ity.ity
  2. | SameType
  3. | NoOver
val overload_of_rs : Expr.rsymbol -> overload
val ref_attr : Ident.attribute
exception IncompatibleNotation of string
type pmodule = private {
  1. mod_theory : Theory.theory;
  2. mod_units : mod_unit list;
  3. mod_export : namespace;
  4. mod_known : Pdecl.known_map;
  5. mod_local : Ident.Sid.t;
  6. mod_used : Ident.Sid.t;
}
and mod_unit =
  1. | Udecl of Pdecl.pdecl
  2. | Uuse of pmodule
  3. | Uclone of mod_inst
  4. | Umeta of Theory.meta * Theory.meta_arg list
  5. | Uscope of string * mod_unit list
val empty_mod_inst : pmodule -> mod_inst
type pmodule_uc = private {
  1. muc_theory : Theory.theory_uc;
  2. muc_units : mod_unit list;
  3. muc_import : namespace list;
  4. muc_export : namespace list;
  5. muc_known : Pdecl.known_map;
  6. muc_local : Ident.Sid.t;
  7. muc_used : Ident.Sid.t;
  8. muc_env : Env.env;
}
val create_module : Env.env -> ?path:string list -> Ident.preid -> pmodule_uc
val close_module : pmodule_uc -> pmodule
val open_scope : pmodule_uc -> string -> pmodule_uc
val close_scope : pmodule_uc -> import:bool -> pmodule_uc
val import_scope : pmodule_uc -> string list -> pmodule_uc
val restore_path : Ident.ident -> string list * string * string list
val restore_module_id : Ident.ident -> pmodule
val restore_module : Theory.theory -> pmodule
val use_export : pmodule_uc -> pmodule -> pmodule_uc
val clone_export : pmodule_uc -> pmodule -> mod_inst -> pmodule_uc
val add_meta : pmodule_uc -> Theory.meta -> Theory.meta_arg list -> pmodule_uc
val add_pdecl : ?warn:bool -> vc:bool -> pmodule_uc -> Pdecl.pdecl -> pmodule_uc
val builtin_module : pmodule
val bool_module : pmodule
val unit_module : pmodule
val highord_module : pmodule
val tuple_module : int -> pmodule
val ref_module : pmodule
val its_ref : Ity.itysymbol
val ts_ref : Ty.tysymbol
val rs_ref : Expr.rsymbol
val rs_ref_cons : Expr.rsymbol
val rs_ref_proj : Expr.rsymbol
val ls_ref_cons : Term.lsymbol
val ls_ref_proj : Term.lsymbol
type mlw_file = pmodule Wstdlib.Mstr.t
val mlw_language : mlw_file Env.language
val mlw_language_builtin : Env.pathname -> mlw_file
exception ModuleNotFound of Env.pathname * string
val read_module : Env.env -> Env.pathname -> string -> pmodule
val print_unit : Format.formatter -> mod_unit -> unit
val print_module : Format.formatter -> pmodule -> unit
OCaml

Innovation. Community. Security.