sig
  val section : Util.Section.t
  type constructor = { cstor_name : ID.t; cstor_ty : Type.t; }
  type t = private {
    ty_id : ID.t;
    ty_vars : Type.t HVar.t list;
    ty_pattern : Type.t;
    ty_constructors : Ind_ty.constructor list;
  }
  exception InvalidDecl of string
  exception NotAnInductiveType of ID.t
  exception NotAnInductiveConstructor of ID.t
  val declare_ty :
    ID.t -> ty_vars:Type.t HVar.t list -> Ind_ty.constructor list -> Ind_ty.t
  val as_inductive_ty : ID.t -> Ind_ty.t option
  val as_inductive_ty_exn : ID.t -> Ind_ty.t
  val is_inductive_ty : ID.t -> bool
  val as_inductive_type : Type.t -> Ind_ty.t option
  val is_inductive_type : Type.t -> bool
  val is_constructor : ID.t -> bool
  val as_constructor : ID.t -> (Ind_ty.constructor * Ind_ty.t) option
  val as_constructor_exn : ID.t -> Ind_ty.constructor * Ind_ty.t
  val contains_inductive_types : FOTerm.t -> bool
  val is_inductive_constant : ID.t -> bool
  val declare_inductive_constant : ID.t -> unit
  val scan_for_constant : ID.t -> Type.t -> unit
  val scan_stmt : ('a, 'b, Type.t, 'c) Statement.t -> unit
  exception Payload_ind_type of Ind_ty.t
  exception Payload_ind_cstor of Ind_ty.constructor * Ind_ty.t
  exception Payload_ind_constant
  exception Payload_ind_projector of ID.t
end