Module Inductive

Extracting an inductive type from a construction
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
type mind_specif = Declarations.mutual_inductive_body * Declarations.one_inductive_body
val lookup_mind_specif : Environ.env -> Names.inductive -> mind_specif

Fetching information in the environment about an inductive type. Raises Not_found if the inductive type is not found.

val ind_subst : Names.MutInd.t -> Declarations.mutual_inductive_body -> Univ.Instance.t -> Constr.constr list
val inductive_paramdecls : Declarations.mutual_inductive_body Univ.puniverses -> Constr.rel_context
val instantiate_inductive_constraints : Declarations.mutual_inductive_body -> Univ.Instance.t -> Univ.Constraint.t
val constrained_type_of_inductive : Environ.env -> mind_specif Univ.puniverses -> Constr.types Univ.constrained
val constrained_type_of_inductive_knowing_parameters : Environ.env -> mind_specif Univ.puniverses -> Constr.types Stdlib.Lazy.t array -> Constr.types Univ.constrained
val relevance_of_inductive : Environ.env -> Names.inductive -> Sorts.relevance
val type_of_inductive : Environ.env -> mind_specif Univ.puniverses -> Constr.types
val type_of_inductive_knowing_parameters : Environ.env -> ?⁠polyprop:bool -> mind_specif Univ.puniverses -> Constr.types Stdlib.Lazy.t array -> Constr.types
val elim_sort : mind_specif -> Sorts.family
val is_private : mind_specif -> bool
val is_primitive_record : mind_specif -> bool
val constrained_type_of_constructor : Constr.pconstructor -> mind_specif -> Constr.types Univ.constrained
val type_of_constructor : Constr.pconstructor -> mind_specif -> Constr.types
val arities_of_constructors : Constr.pinductive -> mind_specif -> Constr.types array

Return constructor types in normal form

val type_of_constructors : Constr.pinductive -> mind_specif -> Constr.types array

Return constructor types in user form

val arities_of_specif : Names.MutInd.t Univ.puniverses -> mind_specif -> Constr.types array

Transforms inductive specification into types (in nf)

val inductive_params : mind_specif -> int
val type_case_branches : Environ.env -> (Constr.pinductive * Constr.constr list) -> Environ.unsafe_judgment -> Constr.constr -> Constr.types array * Constr.types

type_case_branches env (I,args) (p:A) c computes useful types about the following Cases expression: <p>Cases (c :: (I args)) of b1..bn end It computes the type of every branch (pattern variables are introduced by products), the type for the whole expression, and the universe constraints generated.

val build_branches_type : Constr.pinductive -> (Declarations.mutual_inductive_body * Declarations.one_inductive_body) -> Constr.constr list -> Constr.constr -> Constr.types array
val mind_arity : Declarations.one_inductive_body -> Constr.rel_context * Sorts.family

Return the arity of an inductive type

val inductive_sort_family : Declarations.one_inductive_body -> Sorts.family
val check_case_info : Environ.env -> Constr.pinductive -> Sorts.relevance -> Constr.case_info -> unit

Check a case_info actually correspond to a Case expression on the given inductive type.

Guard conditions for fix and cofix-points.
val check_fix : Environ.env -> Constr.fixpoint -> unit

When chk is false, the guard condition is not actually checked.

val check_cofix : Environ.env -> Constr.cofixpoint -> unit
Support for sort-polymorphic inductive types
exception SingletonInductiveBecomesProp of Names.Id.t
val max_inductive_sort : Sorts.t array -> Univ.Universe.t
val instantiate_universes : Environ.env -> Constr.rel_context -> Declarations.template_arity -> Constr.constr Stdlib.Lazy.t array -> Constr.rel_context * Sorts.t
Debug
type size =
| Large
| Strict
type subterm_spec =
| Subterm of size * Declarations.wf_paths
| Dead_code
| Not_subterm
type guard_env = {
env : Environ.env;

dB of last fixpoint

rel_min : int;

dB of variables denoting subterms

genv : subterm_spec Stdlib.Lazy.t list;
}
type stack_element =
| SClosure of guard_env * Constr.constr
| SArg of subterm_spec Stdlib.Lazy.t
val subterm_specif : guard_env -> stack_element list -> Constr.constr -> subterm_spec
val lambda_implicit_lift : int -> Constr.constr -> Constr.constr
val abstract_mind_lc : int -> Int.t -> (Constr.rel_context * Constr.constr) array -> Constr.constr array