DeclareopsSourceOperations concerning types in Declarations : constant_body, mutual_inductive_body, module_body ...
val abstract_universes :
Entries.universes_entry ->
UVars.sort_level_subst * Declarations.universesval map_decl_arity :
('a -> 'c) ->
('b -> 'd) ->
('a, 'b) Declarations.declaration_arity ->
('c, 'd) Declarations.declaration_arityval subst_const_body :
Mod_subst.substitution ->
Declarations.constant_body ->
Declarations.constant_bodyIs there a actual body in const_body ?
val constant_polymorphic_context :
('a, 'b) Declarations.pconstant_body ->
UVars.AbstractContext.tIs the constant polymorphic?
Return the universe context, in case the definition is polymorphic, otherwise the context is empty.
val mk_paths :
Declarations.recarg ->
Declarations.wf_paths list array ->
Declarations.wf_pathsval subst_mind_body :
Mod_subst.substitution ->
Declarations.mutual_inductive_body ->
Declarations.mutual_inductive_bodyval subst_rewrite_rules :
Mod_subst.substitution ->
Declarations.rewrite_rules_body ->
Declarations.rewrite_rules_bodyval inductive_polymorphic_context :
Declarations.mutual_inductive_body ->
UVars.AbstractContext.tIs the inductive polymorphic?
Is the inductive cumulative?
Is the inductive cumulative?
val inductive_make_projection :
Names.inductive ->
Declarations.mutual_inductive_body ->
proj_arg:int ->
Names.Projection.Repr.t * Sorts.relevanceAnomaly when not a primitive record or invalid proj_arg
val inductive_make_projections :
Names.inductive ->
Declarations.mutual_inductive_body ->
(Names.Projection.Repr.t * Sorts.relevance) array optionA default, safe set of flags for kernel type-checking
Here, strictly speaking, we don't perform true hash-consing of the structure, but simply hash-cons all inner constr and other known elements
val hcons_const_body :
('a, 'b) Declarations.pconstant_body ->
('a, 'b) Declarations.pconstant_body