package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/rocq-runtime.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 optionModules
Kernel 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 :
?hbody:(Constr.t -> Constr.t) ->
('a, 'b) Declarations.pconstant_body ->
('a, 'b) Declarations.pconstant_bodySource
val hcons_generic_module_body :
'a Declarations.generic_module_body ->
'a Declarations.generic_module_bodyOn This Page