Module `ComInductive`

type uniform_inductive_flag = | UniformParameters | NonUniformParameters

val do_mutual_inductive : template:bool option -> Constrexpr.universe_decl_expr option -> (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> cumulative:bool -> poly:bool -> private_ind:bool -> uniform:uniform_inductive_flag -> Declarations.recursivity_kind -> unit

val make_cases : Names.inductive -> string list list
val declare_mutual_inductive_with_eliminations : ?⁠primitive_expected:bool -> Entries.mutual_inductive_entry -> UnivNames.universe_binders -> DeclareInd.one_inductive_impls list -> Names.MutInd.t
val interp_mutual_inductive_constr : sigma:Evd.evar_map -> template:bool option -> udecl:UState.universe_decl -> 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_binders

val should_auto_template : Names.Id.t -> bool -> bool: 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 -> bool: template_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_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.