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