Module ComInductive

Inductive and coinductive types
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 -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> Decl_kinds.private_flag -> uniform:uniform_inductive_flag -> Declarations.recursivity_kind -> unit
type one_inductive_impls = Impargs.manual_implicits * Impargs.manual_implicits list
val declare_mutual_inductive_with_eliminations : ?⁠primitive_expected:bool -> Entries.mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list -> Names.MutInd.t
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 : Environ.env -> ctor_levels:Univ.LSet.t -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool

template_polymorphism_candidate env ~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. If the Template Check flag is false we just check that the conclusion sort is not small.

val sign_level : Environ.env -> Evd.evar_map -> Constr.rel_declaration list -> Univ.Universe.t

sign_level env sigma ctx computes the universe level of the context ctx as the sup of its individual assumptions, which should be well-typed in env and sigma

type structured_one_inductive_expr = {
ind_name : Names.Id.t;
ind_arity : Constrexpr.constr_expr;
ind_lc : (Names.Id.t * Constrexpr.constr_expr) list;
}
type structured_inductive_expr = Constrexpr.local_binder_expr list * structured_one_inductive_expr list
val extract_mutual_inductive_declaration_components : (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> structured_inductive_expr * Libnames.qualid list * Vernacexpr.decl_notation list
val interp_mutual_inductive : template:bool option -> Constrexpr.universe_decl_expr option -> structured_inductive_expr -> Vernacexpr.decl_notation list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> Decl_kinds.private_flag -> Declarations.recursivity_kind -> Entries.mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list