sig
  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 option;
  }
  val create_plain_record_decl :
    priv:bool ->
    mut:bool ->
    Ident.preid ->
    Ty.tvsymbol list ->
    (bool * Ity.pvsymbol) list ->
    Term.term list -> Expr.expr option -> Pdecl.its_defn
  val create_rec_record_decl :
    Ity.itysymbol -> Ity.pvsymbol list -> Pdecl.its_defn
  val create_plain_variant_decl :
    Ident.preid ->
    Ty.tvsymbol list ->
    (Ident.preid * (bool * Ity.pvsymbol) list) list -> Pdecl.its_defn
  val create_rec_variant_decl :
    Ity.itysymbol ->
    (Ident.preid * (bool * Ity.pvsymbol) list) list -> Pdecl.its_defn
  val create_alias_decl :
    Ident.preid -> Ty.tvsymbol list -> Ity.ity -> Pdecl.its_defn
  val create_range_decl : Ident.preid -> Number.int_range -> Pdecl.its_defn
  val create_float_decl :
    Ident.preid -> Number.float_format -> Pdecl.its_defn
  type pdecl = private {
    pd_node : Pdecl.pdecl_node;
    pd_pure : Decl.decl list;
    pd_meta : Pdecl.meta_decl list;
    pd_syms : Ident.Sid.t;
    pd_news : Ident.Sid.t;
    pd_tag : int;
  }
  and pdecl_node = private
      PDtype of Pdecl.its_defn list
    | PDlet of Expr.let_defn
    | PDexn of Ity.xsymbol
    | PDpure
  and meta_decl = Theory.meta * Theory.meta_arg list
  val axiom_of_invariant : Pdecl.its_defn -> Term.term
  val meta_depends : Theory.meta
  val create_type_decl : Pdecl.its_defn list -> Pdecl.pdecl list
  val create_let_decl : Expr.let_defn -> Pdecl.pdecl
  val create_exn_decl : Ity.xsymbol -> Pdecl.pdecl
  val create_pure_decl : Decl.decl -> Pdecl.pdecl
  val pd_int : Pdecl.pdecl
  val pd_real : Pdecl.pdecl
  val pd_equ : Pdecl.pdecl
  val pd_ignore_term : Pdecl.pdecl
  val pd_bool : Pdecl.pdecl
  val pd_str : Pdecl.pdecl
  val pd_tuple : int -> Pdecl.pdecl
  val pd_func : Pdecl.pdecl
  val pd_func_app : Pdecl.pdecl
  type known_map = Pdecl.pdecl Ident.Mid.t
  val known_id : Pdecl.known_map -> Ident.ident -> unit
  val known_add_decl : Pdecl.known_map -> Pdecl.pdecl -> Pdecl.known_map
  val merge_known : Pdecl.known_map -> Pdecl.known_map -> Pdecl.known_map
  val find_its_defn : Pdecl.known_map -> Ity.itysymbol -> Pdecl.its_defn
  val print_pdecl : Stdlib.Format.formatter -> Pdecl.pdecl -> unit
end