package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2
doc/coq-core.kernel/Declareops/index.html
Module DeclareopsSource
Operations concerning types in Declarations : constant_body, mutual_inductive_body, module_body ...
Source
val abstract_universes :
Entries.universes_entry ->
UVars.sort_level_subst * Declarations.universesArities
Source
val map_decl_arity :
('a -> 'c) ->
('b -> 'd) ->
('a, 'b) Declarations.declaration_arity ->
('c, 'd) Declarations.declaration_arityConstants
Source
val subst_const_body :
Mod_subst.substitution ->
Declarations.constant_body ->
Declarations.constant_bodyIs there a actual body in const_body ?
Source
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.
Inductive types
Source
val mk_paths :
Declarations.recarg ->
Declarations.wf_paths list array ->
Declarations.wf_pathsSource
val subst_mind_body :
Mod_subst.substitution ->
Declarations.mutual_inductive_body ->
Declarations.mutual_inductive_bodySource
val subst_rewrite_rules :
Mod_subst.substitution ->
Declarations.rewrite_rules_body ->
Declarations.rewrite_rules_bodySource
val inductive_polymorphic_context :
Declarations.mutual_inductive_body ->
UVars.AbstractContext.tIs the inductive polymorphic?
Is the inductive cumulative?
Is the inductive cumulative?
Source
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
Source
val inductive_make_projections :
Names.inductive ->
Declarations.mutual_inductive_body ->
(Names.Projection.Repr.t * Sorts.relevance) array optionKernel 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, 'b) Declarations.pconstant_body ->
('a, 'b) Declarations.pconstant_bodyOn This Page