type its_defn = private {itd_its : Ity.itysymbol;itd_fields : Expr.rsymbol list;itd_constructors : Expr.rsymbol list;itd_invariant : Term.term list;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_defnval create_rec_record_decl : Ity.itysymbol -> Ity.pvsymbol list -> its_defnval create_plain_variant_decl :
Ident.preid ->
Ty.tvsymbol list ->
(Ident.preid * (bool * Ity.pvsymbol) list) list ->
its_defnval create_rec_variant_decl :
Ity.itysymbol ->
(Ident.preid * (bool * Ity.pvsymbol) list) list ->
its_defnval create_alias_decl : Ident.preid -> Ty.tvsymbol list -> Ity.ity -> its_defnval create_range_decl : Ident.preid -> Number.int_range -> its_defnval create_float_decl : Ident.preid -> Number.float_format -> its_defntype pdecl = private {pd_node : pdecl_node;pd_pure : Decl.decl list;pd_meta : meta_decl list;pd_syms : Ident.Sid.t;pd_news : Ident.Sid.t;pd_tag : int;}and pdecl_node = private | PDtype of its_defn list| PDlet of Expr.let_defn| PDexn of Ity.xsymbol| PDpureand meta_decl = Theory.meta * Theory.meta_arg listval create_let_decl : Expr.let_defn -> pdeclval create_exn_decl : Ity.xsymbol -> pdeclval pd_int : pdeclval pd_real : pdeclval pd_equ : pdeclval pd_bool : pdeclval pd_str : pdeclval pd_tuple : int -> pdeclval pd_func : pdeclval pd_func_app : pdecltype known_map = pdecl Ident.Mid.tval known_id : known_map -> Ident.ident -> unitval find_its_defn : known_map -> Ity.itysymbol -> its_defnval print_pdecl : Format.formatter -> pdecl -> unit