Module `ComInductive`

type uniform_inductive_flag = | UniformParameters | NonUniformParameters

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 -> unit

module Mind_decl : sig ... end

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.t: elaborates 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.t, EConstr.t) Context.Rel.Declaration.pt list -> indnames:Names.Id.t list -> arities:EConstr.t list -> arityconcl:EConstr.ESorts.t option 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 -> Entries.mutual_inductive_entry * UnivNames.universe_binders * Univ.ContextSet.t: the post-elaboration part of interp_mutual_inductive, mainly dealing with universe levels

val compute_template_inductive : user_template:bool option -> env_ar_params:Environ.env -> ctx_params:(Constr.constr, Constr.constr) Context.Rel.Declaration.pt list -> univ_entry:UState.universes_entry -> Entries.one_inductive_entry -> Sorts.t option -> 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