Module Alba_core.InductiveSource

Sourcetype params = (string * Term.typ) array
Sourcemodule Header : sig ... end
Sourcemodule Constructor : sig ... end
Sourcemodule Type : sig ... end
Sourcetype t
Sourceval make : params -> Fmlib.Common.Int_set.t -> Type.t array -> t
Sourceval up : int -> t -> t
Sourceval count_types : t -> int
Sourceval count_params : t -> int
Sourceval is_param_positive : int -> t -> bool
Sourceval parameter_name : int -> t -> string
Sourceval parameters : t -> params
Sourceval ith_type : int -> t -> string * Term.typ
Sourceval count_constructors : int -> t -> int
Sourceval count_previous_constructors : int -> t -> int
Sourceval 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.

Sourceval 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.