Ind

Ltac2.Ind

type t = inductive

An inductive is the name of a mutually inductive type, along with the index of an inductive block within that type.

type data = inductive * Declarations.mutual_inductive_body

The actual data specified by a concrete declaration of an inductive type, containing, e.g., its constructors and its parameters. A value of type data corresponds to one inductive type within a larger mutually inductive block.

val equal : t -> t -> bool

Equality test for inductives.

val data : Environ.env -> t -> data

data env ind gets the data of ind in the environment env.

val repr : data -> t

repr data returns the name of the inductive type corresponding to the block. Inverse of data.

val index : t -> int

index ind returns the index of the inductive type inside its mutual block. Guaranteed to range between 0 and nblocks data - 1 where data was retrieved using the above function.

val nblocks : data -> int

nblocks data returns the number of inductive types appearing in a mutual block.

val nconstructors : data -> int

nconstructors data returns the number of constructors appearing in the current block.

val get_block : data -> int -> data option

get_block data n is the block corresponding to the nth inductive type in data's parent mutually inductive type. Index must range between 0 and nblocks data - 1, otherwise the function returns None.

val get_constructor : data -> int -> constructor option

get_constructor data n returns the nth constructor of the inductive type. Index must range between 0 and nconstructors data - 1, otherwise the function returns None.

val nparams : data -> int

nparams data returns the number of parameters of the inductive type, including both uniform and non-uniform parameters. Does not count local let-ins.

val nparams_uniform : data -> int

nparams_uniform data returns the number of recursively uniform (i.e., ordinary) parameters of the inductive type.

val get_projections : data -> projection array option

get_projections data returns the list of projections for a primitive record, or None if the inductive is not a primitive record.

val constructor_nargs : data -> int array

(constructor_nargs data).(n) is the number of non-parameter arguments accepted by the nth constructor of this inductive type. Add (constructor_nargs data).(n) to nparams data to get the total number of arguments of the constructor.

val constructor_ndecls : data -> int array

(constructor_ndecls data).(n) is the number of variables bound in a pattern match expression by the nth constructor of this inductive type. Can be greater than constructor_nargs data if the constructors have local let-bindings, e.g., applied to Inductive Ind (A : Type) (f : A -> A) : Set := Constr (x : A) (y := f x) it would return [|2|], because in match t with Constr _ _ x y => e end, x and y are bound in e.

val print : t -> message

print ind prints the inductive using the shortest qualified identifier which refers to it. Does not avoid variable names in the current or global environment.