Module Inductiveops

The following three functions are similar to the ones defined in Inductive, but they expect an env

Return type as quoted by the user

val type_of_constructors : Environ.env -> Names.inductive Evd.puniverses -> EConstr.types array
val arities_of_constructors : Environ.env -> Names.inductive Evd.puniverses -> EConstr.types array

Return constructor types in normal form

type inductive_family

An inductive type with its parameters (transparently supports reasoning either with only recursively uniform parameters or with all parameters including the recursively non-uniform ones

val liftn_inductive_family : int -> int -> inductive_family -> inductive_family
val lift_inductive_family : int -> inductive_family -> inductive_family
val substnl_ind_family : EConstr.constr list -> int -> inductive_family -> inductive_family
val relevance_of_inductive_family : Environ.env -> inductive_family -> EConstr.ERelevance.t
type inductive_type =
  1. | IndType of inductive_family * EConstr.constr list

An inductive type with its parameters and real arguments

val make_ind_type : (inductive_family * EConstr.constr list) -> inductive_type
val dest_ind_type : inductive_type -> inductive_family * EConstr.constr list
val map_inductive_type : (EConstr.constr -> EConstr.constr) -> inductive_type -> inductive_type
val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
val lift_inductive_type : int -> inductive_type -> inductive_type
val substnl_ind_type : EConstr.constr list -> int -> inductive_type -> inductive_type
val ind_of_ind_type : inductive_type -> Names.inductive
val relevance_of_inductive_type : Environ.env -> inductive_type -> EConstr.ERelevance.t
val mkAppliedInd : inductive_type -> EConstr.constr
val mis_is_recursive : Declarations.one_inductive_body -> bool

Check if a one_inductive_body is recursive, possibly nestedly

Extract information from an inductive name
val nconstructors : Environ.env -> Names.inductive -> int
  • returns

    number of constructors

val constructors_nrealargs : Environ.env -> Names.inductive -> int array
  • returns

    arity of constructors excluding parameters, excluding local defs

val constructors_nrealdecls : Environ.env -> Names.inductive -> int array
  • returns

    arity of constructors excluding parameters, including local defs

val inductive_nrealargs : Environ.env -> Names.inductive -> int
  • returns

    the arity, excluding params, excluding local defs

val inductive_nrealdecls : Environ.env -> Names.inductive -> int
  • returns

    the arity, excluding params, including local defs

val inductive_nallargs : Environ.env -> Names.inductive -> int
  • returns

    the arity, including params, excluding local defs

val inductive_nalldecls : Environ.env -> Names.inductive -> int
  • returns

    the arity, including params, including local defs

val inductive_nparams : Environ.env -> Names.inductive -> int
  • returns

    nb of params without local defs

val inductive_nparamdecls : Environ.env -> Names.inductive -> int
  • returns

    nb of params with local defs

  • returns

    params context

  • returns

    full arity context, hence with letin

Extract information from a constructor name
val constructor_nallargs : Environ.env -> Names.constructor -> int
  • returns

    param + args without letin

val constructor_nalldecls : Environ.env -> Names.constructor -> int
  • returns

    param + args with letin

val constructor_nrealargs : Environ.env -> Names.constructor -> int
  • returns

    args without letin

val constructor_nrealdecls : Environ.env -> Names.constructor -> int
  • returns

    args with letin

val inductive_alltags : Environ.env -> Names.inductive -> bool list
  • returns

    tags of all decls: true = letin, false = assumption

val constructor_alltags : Environ.env -> Names.constructor -> bool list
val inductive_has_local_defs : Environ.env -> Names.inductive -> bool

Is there local defs in params or args ?

val constant_sorts_below : UnivGen.QualityOrSet.t -> UnivGen.QualityOrSet.t list
val sorts_for_schemes : Declarations.mind_specif -> UnivGen.QualityOrSet.t list

Take into account elimination constraints. When there is an elimination constraint and the predicate is underspecified, i.e. a QSort, we make a non-canonical choice for the return type. Incompatible constraints produce a universe inconsistency.

val is_allowed_elimination : Evd.evar_map -> (Declarations.mind_specif * EConstr.EInstance.t) -> EConstr.ESorts.t -> bool

Returns Some sigma' if the elimination can be allowed, possibly adding constraints in sigma'

val has_dependent_elim : Evd.evar_map -> Declarations.mind_specif -> EConstr.EInstance.t -> bool

(Co)Inductive records with primitive projections do not have eta-conversion, hence no dependent elimination.

val always_dependent_elim : Declarations.mind_specif -> bool
val type_of_projection_knowing_arg : Environ.env -> Evd.evar_map -> Names.Projection.t -> EConstr.t -> EConstr.types -> EConstr.types

Primitive projections

Extract information from an inductive family

type constructor_summary = {
  1. cs_name : Names.Id.t;
  2. cs_cstr : Names.constructor Evd.puniverses;
  3. cs_params : EConstr.constr list;
  4. cs_nargs : int;
  5. cs_args : EConstr.rel_context;
  6. cs_concl_realargs : EConstr.constr array;
}
val lift_constructor : int -> constructor_summary -> constructor_summary
val get_constructors : Environ.env -> inductive_family -> constructor_summary array

get_arity returns the arity of the inductive family instantiated with the parameters; if recursively non-uniform parameters are not part of the inductive family, they appears in the arity

val build_dependent_constructor : constructor_summary -> EConstr.constr
val build_dependent_inductive : Environ.env -> inductive_family -> EConstr.constr
val make_arity_signature : Environ.env -> Evd.evar_map -> bool -> inductive_family -> EConstr.rel_context

Raise Not_found if not given a valid inductive type

instantiate_constructor_params cstr mind params instantiates the type of the given constructor with parameters params

val arity_of_case_predicate : Environ.env -> inductive_family -> bool -> EConstr.ESorts.t -> EConstr.types

Builds the case predicate arity (dependent or not)

Annotation for cases

Make a case or substitute projections if the inductive type is a record with primitive projections. Fail with an error if the elimination is dependent while the inductive type does not allow dependent elimination.

Sometimes make_case_or_project is nicer to call with a pre-built case_invert than inductive_type.

val compute_projections : Environ.env -> Names.inductive -> (EConstr.constr * EConstr.types) array

Given a primitive record type, for every field computes the eta-expanded projection and its type.

val control_only_guard : Environ.env -> Evd.evar_map -> EConstr.types -> unit

Generalize template polymorphic universe variables, subtitute the instance, and returns the context of parameters, the new evar_map, and the substitution for the template variable if there is one.

module Internal : sig ... end