Module `Declareops`Source

Operations concerning types in Declarations : constant_body, mutual_inductive_body, module_body ...

Sourceval universes_context : Declarations.universes -> UVars.AbstractContext.t

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

Arities

Source

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

Constants

Source

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

Is there a actual body in const_body ?

Sourceval constant_has_body : 'a Declarations.pconstant_body -> bool

Source

val constant_polymorphic_context : 
  'a Declarations.pconstant_body ->
  UVars.AbstractContext.t

Sourceval constant_is_polymorphic : 'a Declarations.pconstant_body -> bool

Is the constant polymorphic?

Return the universe context, in case the definition is polymorphic, otherwise the context is empty.

Sourceval is_opaque : 'a Declarations.pconstant_body -> bool

Inductive types

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

Sourceval pr_recarg : Declarations.recarg -> Pp.t

Sourceval pr_wf_paths : Declarations.wf_paths -> Pp.t

Source

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

Sourceval mk_norec : Declarations.wf_paths

Source

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

Sourceval dest_recarg : Declarations.wf_paths -> Declarations.recarg

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

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

Source

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

Source

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

Source

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

Sourceval inductive_is_polymorphic : Declarations.mutual_inductive_body -> bool

Is the inductive polymorphic?

Is the inductive cumulative?

Sourceval inductive_is_cumulative : Declarations.mutual_inductive_body -> bool

Is the inductive cumulative?

Source

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

Source

val inductive_make_projections : 
  Names.inductive ->
  Declarations.mutual_inductive_body ->
  (Names.Projection.Repr.t * Sorts.relevance) array option

Kernel flags

Sourceval safe_flags : Conv_oracle.oracle -> Declarations.typing_flags

A default, safe set of flags for kernel type-checking

Hash-consing

Here, strictly speaking, we don't perform true hash-consing of the structure, but simply hash-cons all inner constr and other known elements

Source

val hcons_const_body : 
  'a Declarations.pconstant_body ->
  'a Declarations.pconstant_body

Source

val hcons_mind : 
  Declarations.mutual_inductive_body ->
  Declarations.mutual_inductive_body

Sourceval hcons_module_body : Declarations.module_body -> Declarations.module_body

Source

val hcons_module_type : 
  Declarations.module_type_body ->
  Declarations.module_type_body

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/Declareops/index.html

Module `Declareops`Source

Arities

Constants

Inductive types

Kernel flags

Hash-consing

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/Declareops/index.html

Module DeclareopsSource

Arities

Constants

Inductive types

Kernel flags

Hash-consing

Module `Declareops`Source