DeclareopsOperations concerning types in Declarations : constant_body, mutual_inductive_body, module_body ...
val universes_context : Declarations.universes -> UVars.AbstractContext.tval 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_has_body : ('a, 'b) Declarations.pconstant_body -> boolval constant_polymorphic_context : ('a, 'b) Declarations.pconstant_body -> UVars.AbstractContext.tval constant_is_polymorphic : ('a, 'b) Declarations.pconstant_body -> boolIs the constant polymorphic?
Return the universe context, in case the definition is polymorphic, otherwise the context is empty.
val is_opaque : ('a, 'b) Declarations.pconstant_body -> boolval eq_recarg : Declarations.recarg -> Declarations.recarg -> boolval pr_recarg : Declarations.recarg -> Pp.tval pr_wf_paths : Declarations.wf_paths -> Pp.tval subst_recarg : Mod_subst.substitution -> Declarations.recarg -> Declarations.recargval mk_norec : Declarations.wf_pathsval mk_paths : Declarations.recarg -> Declarations.wf_paths list array -> Declarations.wf_pathsval dest_recarg : Declarations.wf_paths -> Declarations.recargval dest_subterms : Declarations.wf_paths -> Declarations.wf_paths list arrayval recarg_length : Declarations.wf_paths -> int -> intval subst_wf_paths : Mod_subst.substitution -> Declarations.wf_paths -> 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.tval inductive_is_polymorphic : Declarations.mutual_inductive_body -> boolIs the inductive polymorphic?
Is the inductive cumulative?
val inductive_is_cumulative : Declarations.mutual_inductive_body -> boolIs 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 optionval safe_flags : Conv_oracle.oracle -> Declarations.typing_flagsA 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 : ?hbody:(Constr.t -> Constr.t) -> ('a, 'b) Declarations.pconstant_body -> ('a, 'b) Declarations.pconstant_bodyval hcons_mind : Declarations.mutual_inductive_body -> Declarations.mutual_inductive_bodyval hcons_module_body : Declarations.module_body -> Declarations.module_bodyval hcons_module_type : Declarations.module_type_body -> Declarations.module_type_body