Module `Inductive`

val find_rectype : Environ.env -> Constr.types -> Constr.pinductive * Constr.constr list
val find_inductive : Environ.env -> Constr.types -> Constr.pinductive * Constr.constr list
val find_coinductive : Environ.env -> Constr.types -> Constr.pinductive * Constr.constr list
val lookup_mind_specif : Environ.env -> Names.inductive -> Declarations.mind_specif: Fetching information in the environment about an inductive type. Raises an anomaly if the inductive type is not found.

val inductive_paramdecls : Declarations.mutual_inductive_body UVars.puniverses -> Constr.rel_context: Returns the parameters of an inductive type with universes instantiated

val inductive_nonrec_rec_paramdecls : Declarations.mutual_inductive_body UVars.puniverses -> Constr.rel_context * Constr.rel_context: Returns the parameters of an inductive type with universes instantiated, splitting it into the contexts of recursively uniform and recursively non-uniform parameters

val instantiate_inductive_constraints : Declarations.mutual_inductive_body -> UVars.Instance.t -> Univ.Constraints.t

type template_univ = | TemplateProp | TemplateUniv of Univ.Universe.t
type param_univs = (expected:Univ.Level.t -> template_univ) list

val constrained_type_of_inductive : Declarations.mind_specif UVars.puniverses -> Constr.types Univ.constrained
val constrained_type_of_inductive_knowing_parameters : Declarations.mind_specif UVars.puniverses -> param_univs -> Constr.types Univ.constrained
val relevance_of_ind_body : Declarations.one_inductive_body -> UVars.Instance.t -> Sorts.relevance
val relevance_of_inductive : Environ.env -> Constr.pinductive -> Sorts.relevance
val type_of_inductive : Declarations.mind_specif UVars.puniverses -> Constr.types
val type_of_inductive_knowing_parameters : ?⁠polyprop:bool -> Declarations.mind_specif UVars.puniverses -> param_univs -> Constr.types
val quality_leq : Sorts.Quality.t -> Sorts.Quality.t -> bool: For squashing.

type squash = | SquashToSet | SquashToQuality of Sorts.Quality.t

val is_squashed : Declarations.mind_specif UVars.puniverses -> squash option
val is_allowed_elimination : Declarations.mind_specif UVars.puniverses -> Sorts.t -> bool
val is_private : Declarations.mind_specif -> bool
val is_primitive_record : Declarations.mind_specif -> bool

val constrained_type_of_constructor : Constr.pconstructor -> Declarations.mind_specif -> Constr.types Univ.constrained
val type_of_constructor : Constr.pconstructor -> Declarations.mind_specif -> Constr.types
val arities_of_constructors : Constr.pinductive -> Declarations.mind_specif -> Constr.types array: Return constructor types in normal form

val type_of_constructors : Constr.pinductive -> Declarations.mind_specif -> Constr.types array: Return constructor types in user form

val abstract_constructor_type_relatively_to_inductive_types_context : int -> Names.MutInd.t -> Constr.types -> Constr.types: Turns a constructor type recursively referring to inductive types into the same constructor type referring instead to a context made from the abstract declaration of the inductive types (e.g. turns nat->nat into mkArrowR (Rel 1) (Rel 2)); takes as arguments the number of inductive types in the block and the name of the block

val inductive_params : Declarations.mind_specif -> int
val expand_arity : Declarations.mind_specif -> Constr.pinductive -> Constr.constr array -> Names.Name.t Context.binder_annot array -> Constr.rel_context: Given an inductive type and its parameters, builds the context of the return clause, including the inductive being eliminated. The additional binder array is only used to set the names of the context variables, we use the less general type to make it easy to use this function on Case nodes.

type ('constr, 'types) pexpanded_case = Constr.case_info * ('constr * Sorts.relevance) * 'constr Constr.pcase_invert * 'constr * 'constr array
type expanded_case = (Constr.constr, Constr.types) pexpanded_case

val expand_case : Environ.env -> Constr.case -> expanded_case: Given a pattern-matching represented compactly, expands it so as to produce lambda and let abstractions in front of the return clause and the pattern branches.

val expand_case_specif : Declarations.mutual_inductive_body -> Constr.case -> expanded_case
val contract_case : Environ.env -> expanded_case -> Constr.case: Dual operation of the above. Fails if the return clause or branch has not the expected form.

val instantiate_context : UVars.Instance.t -> Vars.substl -> Names.Name.t Context.binder_annot array -> Constr.rel_context -> Constr.rel_context: instantiate_context u subst nas ctx applies both u and subst to ctx while replacing names using nas (order reversed). In particular, assumes that ctx and nas have the same length.

val build_branches_type : Constr.pinductive -> (Declarations.mutual_inductive_body * Declarations.one_inductive_body) -> Constr.constr list -> Constr.constr -> Constr.types array
val inductive_sort_family : Declarations.one_inductive_body -> Sorts.family: Return the arity of an inductive type

val check_case_info : Environ.env -> Constr.pinductive -> Constr.case_info -> unit: Check a case_info actually correspond to a Case expression on the given inductive type.

val is_primitive_positive_container : Environ.env -> Names.Constant.t -> bool: is_primitive_positive_container env c tells if the constant c is registered as a primitive type that can be seen as a container where the occurrences of its parameters are positive, in which case the positivity and guard conditions are extended to allow inductive types to nest their subterms in these containers.

val check_fix : Environ.env -> Constr.fixpoint -> unit: When chk is false, the guard condition is not actually checked.

val abstract_mind_lc : int -> int -> Names.MutInd.t -> (Constr.rel_context * Constr.constr) array -> Constr.constr array