Module `Declareops`

val universes_context : Declarations.universes -> UVars.AbstractContext.t
val abstract_universes : Entries.universes_entry -> UVars.sort_level_subst * Declarations.universes

Arities

val map_decl_arity : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) Declarations.declaration_arity -> ('c, 'd) Declarations.declaration_arity

Constants

val subst_const_body : Mod_subst.substitution -> Declarations.constant_body -> Declarations.constant_body

val constant_has_body : 'a Declarations.pconstant_body -> bool
val constant_polymorphic_context : 'a Declarations.pconstant_body -> UVars.AbstractContext.t
val constant_is_polymorphic : 'a Declarations.pconstant_body -> bool: Is the constant polymorphic?

val is_opaque : 'a Declarations.pconstant_body -> bool

Inductive types

val eq_recarg : Declarations.recarg -> Declarations.recarg -> bool

val pr_recarg : Declarations.recarg -> Pp.t

val pr_wf_paths : Declarations.wf_paths -> Pp.t

val subst_recarg : Mod_subst.substitution -> Declarations.recarg -> Declarations.recarg

val mk_norec : Declarations.wf_paths

val mk_paths : Declarations.recarg -> Declarations.wf_paths list array -> Declarations.wf_paths

val dest_recarg : Declarations.wf_paths -> Declarations.recarg

val dest_subterms : Declarations.wf_paths -> Declarations.wf_paths list array

val recarg_length : Declarations.wf_paths -> int -> int

val subst_wf_paths : Mod_subst.substitution -> Declarations.wf_paths -> Declarations.wf_paths

val subst_mind_body : Mod_subst.substitution -> Declarations.mutual_inductive_body -> Declarations.mutual_inductive_body

val inductive_polymorphic_context : Declarations.mutual_inductive_body -> UVars.AbstractContext.t

val inductive_is_polymorphic : Declarations.mutual_inductive_body -> bool

Is the inductive polymorphic?

Is the inductive cumulative?

val inductive_is_cumulative : Declarations.mutual_inductive_body -> bool: Is the inductive cumulative?

val inductive_make_projection : Names.inductive -> Declarations.mutual_inductive_body -> proj_arg:int -> Names.Projection.Repr.t * Sorts.relevance: Anomaly 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 option

Kernel flags

val safe_flags : Conv_oracle.oracle -> Declarations.typing_flags: A default, safe set of flags for kernel type-checking

Hash-consing

val hcons_const_body : 'a Declarations.pconstant_body -> 'a Declarations.pconstant_body
val hcons_mind : Declarations.mutual_inductive_body -> Declarations.mutual_inductive_body
val hcons_module_body : Declarations.module_body -> Declarations.module_body
val hcons_module_type : Declarations.module_type_body -> Declarations.module_type_body