package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c
doc/coq-core.vernac/ComInductive/index.html
Module ComInductiveSource
Inductive and coinductive types
Entry points for the vernacular commands Inductive and CoInductive
val do_mutual_inductive :
template:bool option ->
Constrexpr.cumul_univ_decl_expr option ->
(Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list ->
cumulative:bool ->
poly:bool ->
?typing_flags:Declarations.typing_flags ->
private_ind:bool ->
uniform:uniform_inductive_flag ->
Declarations.recursivity_kind ->
unitUser-interface API
Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name followed by enough pattern variables. Not_found is raised if the given string isn't the qualid of a known inductive type.
val interp_mutual_inductive_constr :
sigma:Evd.evar_map ->
template:bool option ->
udecl:UState.universe_decl ->
variances:Entries.variance_entry ->
ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list ->
indnames:Names.Id.t list ->
arities:EConstr.t list ->
arityconcl:(bool * EConstr.ESorts.t) option list ->
constructors:(Names.Id.t list * Constr.constr list) list ->
env_ar_params:Environ.env ->
cumulative:bool ->
poly:bool ->
private_ind:bool ->
finite:Declarations.recursivity_kind ->
Entries.mutual_inductive_entry * UnivNames.universe_bindersInternal API, exported for Record
should_auto_template x b is true when b is true and we automatically use template polymorphism. x is the name of the inductive under consideration.
val template_polymorphism_candidate :
ctor_levels:Univ.LSet.t ->
Entries.universes_entry ->
Constr.rel_context ->
Sorts.t option ->
booltemplate_polymorphism_candidate ~ctor_levels uctx params conclsort is true iff an inductive with params params, conclusion conclsort and universe levels appearing in the constructor arguments ctor_levels would be definable as template polymorphic. It should have at least one universe in its monomorphic universe context that can be made parametric in its conclusion sort, if one is given.
val maybe_unify_params_in :
Environ.env ->
Evd.evar_map ->
ninds:int ->
nparams:int ->
binders:int ->
EConstr.t ->
Evd.evar_mapnparams is the number of parameters which aren't treated as uniform, ie the length of params (including letins) where the env is uniform params, inductives, params, binders.
val variance_of_entry :
cumulative:bool ->
variances:Entries.variance_entry ->
Entries.universes_entry ->
Entries.variance_entry optionWill return None if non-cumulative, and resize if there are more universes than originally specified. If monomorphic, cumulative is treated as false.