Module Alba_core.Inductive

type params = (string * Term.typ) array
module Header : sig ... end
module Constructor : sig ... end
module Type : sig ... end
type t
val make : params -> Fmlib.Common.Int_set.t -> Type.t array -> t
val up : int -> t -> t
val count_types : t -> int
val count_params : t -> int
val is_param_positive : int -> t -> bool
val parameter_name : int -> t -> string
val parameters : t -> params
val ith_type : int -> t -> string * Term.typ
val count_constructors : int -> t -> int
val count_previous_constructors : int -> t -> int
val raw_constructor : int -> int -> t -> string * Term.typ

raw_constructor i j ind

The name and the type of the jth constructor of the ith inductive type of the family, valid in a context with the inductive types and the parameters.

val constructor : int -> int -> t -> string * Term.typ

constructor i j ind

The name and the type of the jth constructor of the ith inductive type of the family, valid in a context with the inductive types.