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.

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