package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2
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.notation_declaration 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 :
env:Environ.env ->
template:bool option ->
Constrexpr.cumul_univ_decl_expr option ->
(Vernacexpr.one_inductive_expr * Vernacexpr.notation_declaration list) list ->
cumulative:bool ->
poly:bool ->
?typing_flags:Declarations.typing_flags ->
private_ind:bool ->
uniform:uniform_inductive_flag ->
Declarations.recursivity_kind ->
Mind_decl.telaborates an inductive declaration (the first half of do_mutual_inductive)
val interp_mutual_inductive_constr :
sigma:Evd.evar_map ->
template:bool option ->
udecl:UState.universe_decl ->
variances:Entries.variance_entry ->
ctx_params:EConstr.rel_context ->
indnames:Names.Id.t list ->
arities_explicit:bool list ->
arities:EConstr.t list ->
template_syntax:syntax_allows_template_poly list ->
constructors:(Names.Id.t list * EConstr.constr list) list ->
env_ar_params:Environ.env ->
cumulative:bool ->
poly:bool ->
private_ind:bool ->
finite:Declarations.recursivity_kind ->
DeclareInd.default_dep_elim list
* Entries.mutual_inductive_entry
* UnivNames.universe_binders
* Univ.ContextSet.tthe post-elaboration part of interp_mutual_inductive, mainly dealing with universe levels
Internal API, exported for Record
val compute_template_inductive :
user_template:bool option ->
ctx_params:Constr.rel_context ->
univ_entry:UState.universes_entry ->
Entries.one_inductive_entry ->
syntax_allows_template_poly ->
Entries.inductive_universes_entry * Univ.ContextSet.tcompute_template_inductive computes whether an inductive can be template polymorphic.
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.inductive_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.