package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587
doc/coq-core.kernel/Inductive/index.html
Module InductiveSource
Extracting an inductive type from a construction
find_m*type env sigma c coerce c to an recursive type (I args). find_rectype, find_inductive and find_coinductive respectively accepts any recursive type, only an inductive type and only a coinductive type. They raise Not_found if not convertible to a recursive type.
Fetching information in the environment about an inductive type. Raises an anomaly if the inductive type is not found.
Functions to build standard types related to inductive
val inductive_paramdecls :
Declarations.mutual_inductive_body Univ.puniverses ->
Constr.rel_contextReturns the parameters of an inductive type with universes instantiated
val inductive_nonrec_rec_paramdecls :
Declarations.mutual_inductive_body Univ.puniverses ->
Constr.rel_context * Constr.rel_contextReturns 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 ->
Univ.Instance.t ->
Univ.Constraints.tThe 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.constrainedval constrained_type_of_inductive_knowing_parameters :
mind_specif Univ.puniverses ->
param_univs ->
Constr.types Univ.constrainedval type_of_inductive_knowing_parameters :
?polyprop:bool ->
mind_specif Univ.puniverses ->
param_univs ->
Constr.typesReturn type as quoted by the user
val constrained_type_of_constructor :
Constr.pconstructor ->
mind_specif ->
Constr.types Univ.constrainedReturn constructor types in normal form
Return constructor types in user form
val abstract_constructor_type_relatively_to_inductive_types_context :
int ->
Names.MutInd.t ->
Constr.types ->
Constr.typesTurns 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 expand_case :
Environ.env ->
Constr.case ->
Constr.case_info
* Constr.constr
* Constr.case_invert
* Constr.constr
* Constr.constr arrayGiven 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 ->
Constr.case_info
* Constr.constr
* Constr.case_invert
* Constr.constr
* Constr.constr arrayval contract_case :
Environ.env ->
(Constr.case_info
* Constr.constr
* Constr.case_invert
* Constr.constr
* Constr.constr array) ->
Constr.caseDual operation of the above. Fails if the return clause or branch has not the expected form.
val instantiate_context :
Univ.Instance.t ->
Vars.substl ->
Names.Name.t Context.binder_annot array ->
Constr.rel_context ->
Constr.rel_contextinstantiate_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 type_case_branches :
Environ.env ->
(Constr.pinductive * Constr.constr list) ->
Environ.unsafe_judgment ->
Constr.constr ->
Constr.types array * Constr.typestype_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 arrayReturn the arity of an inductive type
val check_case_info :
Environ.env ->
Constr.pinductive ->
Sorts.relevance ->
Constr.case_info ->
unitCheck a case_info actually correspond to a Case expression on the given inductive type.
Guard conditions for fix and cofix-points.
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.
When chk is false, the guard condition is not actually checked.
Support for sort-polymorphic inductive types
The "polyprop" optional argument below controls the "Prop-polymorphism". By default, it is allowed. But when "polyprop=false", the following exception is raised when a polymorphic singleton inductive type becomes Prop due to parameter instantiation. This is used by the Ocaml extraction, which cannot handle (yet?) Prop-polymorphism.
val abstract_mind_lc :
int ->
int ->
Names.MutInd.t ->
(Constr.rel_context * Constr.constr) array ->
Constr.constr array