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