Module ComInductive
Inductive and coinductive types
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 : env0:Environ.env -> sigma:Evd.evar_map -> template:bool option -> udecl:UState.universe_decl -> env_ar:Environ.env -> env_params:Environ.env -> 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 * 'a list 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
istrue
whenb
istrue
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
istrue
iff an inductive with paramsparams
, conclusionconclsort
and universe levels appearing in the constructor argumentsctor_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 theTemplate Check
flag is false we just check that the conclusion sort is not small.