ComInductive
type flags = {
poly : bool; |
cumulative : bool; |
template : bool option; |
auto_prop_lowering : bool; |
finite : Declarations.recursivity_kind; |
mode : Hints.hint_mode list option; |
}
Entry points for the vernacular commands Inductive and CoInductive
val do_mutual_inductive : flags:flags -> ?typing_flags:Declarations.typing_flags ->
Constrexpr.cumul_univ_decl_expr option -> (Vernacexpr.one_inductive_expr * Vernacexpr.notation_declaration list) list -> private_ind:bool -> uniform:uniform_inductive_flag -> unit
User-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 make_cases : Names.inductive -> string list list
module Mind_decl : sig ... end
val interp_mutual_inductive : env:Environ.env -> flags:flags -> ?typing_flags:Declarations.typing_flags ->
Constrexpr.cumul_univ_decl_expr option -> (Vernacexpr.one_inductive_expr * Vernacexpr.notation_declaration list) list -> private_ind:bool -> uniform:uniform_inductive_flag -> Mind_decl.t
elaborates an inductive declaration (the first half of do_mutual_inductive)
val interp_mutual_inductive_constr : sigma:Evd.evar_map -> flags:flags -> 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 ->
private_ind:bool -> DeclareInd.default_dep_elim list * Entries.mutual_inductive_entry * UnivNames.universe_binders * Univ.ContextSet.t
the 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.t
compute_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_map
nparams
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 option
Will return None if non-cumulative, and resize if there are more universes than originally specified. If monomorphic, cumulative
is treated as false
.
module Internal : sig ... end