package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type its_defn = private {
  1. itd_its : Ity.itysymbol;
  2. itd_fields : Expr.rsymbol list;
  3. itd_constructors : Expr.rsymbol list;
  4. itd_invariant : Term.term list;
  5. itd_witness : Expr.expr list;
}
val create_plain_record_decl : priv:bool -> mut:bool -> Ident.preid -> Ty.tvsymbol list -> (bool * Ity.pvsymbol) list -> Term.term list -> Expr.expr list -> its_defn
val create_rec_record_decl : Ity.itysymbol -> Ity.pvsymbol list -> its_defn
val create_plain_variant_decl : Ident.preid -> Ty.tvsymbol list -> (Ident.preid * (bool * Ity.pvsymbol) list) list -> its_defn
val create_rec_variant_decl : Ity.itysymbol -> (Ident.preid * (bool * Ity.pvsymbol) list) list -> its_defn
val create_alias_decl : Ident.preid -> Ty.tvsymbol list -> Ity.ity -> its_defn
val create_range_decl : Ident.preid -> Number.int_range -> its_defn
val create_float_decl : Ident.preid -> Number.float_format -> its_defn
type pdecl = private {
  1. pd_node : pdecl_node;
  2. pd_pure : Decl.decl list;
  3. pd_meta : meta_decl list;
  4. pd_syms : Ident.Sid.t;
  5. pd_news : Ident.Sid.t;
  6. pd_tag : int;
}
and pdecl_node = private
  1. | PDtype of its_defn list
  2. | PDlet of Expr.let_defn
  3. | PDexn of Ity.xsymbol
  4. | PDpure
and meta_decl = Theory.meta * Theory.meta_arg list
val axiom_of_invariant : its_defn -> Term.term
val create_type_decl : its_defn list -> pdecl list
val create_let_decl : Expr.let_defn -> pdecl
val create_exn_decl : Ity.xsymbol -> pdecl
val create_pure_decl : Decl.decl -> pdecl
val pd_int : pdecl
val pd_real : pdecl
val pd_equ : pdecl
val pd_bool : pdecl
val pd_tuple : int -> pdecl
val pd_func : pdecl
val pd_func_app : pdecl
type known_map = pdecl Ident.Mid.t
val known_id : known_map -> Ident.ident -> unit
val known_add_decl : known_map -> pdecl -> known_map
val merge_known : known_map -> known_map -> known_map
val find_its_defn : known_map -> Ity.itysymbol -> its_defn
val print_pdecl : Format.formatter -> pdecl -> unit
OCaml

Innovation. Community. Security.