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

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: Functions to build standard types related to inductive

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 make_param_univs : Environ.env -> Constr.constr array -> param_univs: The constr array is the types of the arguments to a template polymorphic inductive.

val constrained_type_of_inductive : mind_specif Univ.puniverses -> Constr.types Univ.constrained
val constrained_type_of_inductive_knowing_parameters : mind_specif Univ.puniverses -> param_univs -> Constr.types Univ.constrained
val relevance_of_inductive : Environ.env -> Names.inductive -> Sorts.relevance
val type_of_inductive : mind_specif Univ.puniverses -> Constr.types
val type_of_inductive_knowing_parameters : ?⁠polyprop:bool -> mind_specif Univ.puniverses -> param_univs -> 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.

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.

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

`env : Environ.env;`	dB of last fixpoint
`rel_min : int;`	dB of variables denoting subterms
`genv : subterm_spec Stdlib.Lazy.t list;`