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/Constant_typing/index.html
Module Constant_typingSource
Handlers are used to manage side-effects. The 'a type stands for the type of side-effects, and it is parametric because they are only defined later on. Handlers inline the provided side-effects into the term, and return the set of additional global constraints that need to be added for the term to be well typed.
Source
val infer_local_def :
Environ.env ->
Names.Id.t ->
Entries.section_def_entry ->
Constr.constr * Sorts.relevance * Constr.typesSource
val infer_primitive :
Environ.env ->
Entries.primitive_entry ->
('a, unit) Declarations.pconstant_bodySource
val infer_symbol :
Environ.env ->
Entries.symbol_entry ->
('a, unit) Declarations.pconstant_bodySource
val infer_parameter :
sec_univs:UVars.Instance.t option ->
Environ.env ->
Entries.parameter_entry ->
('a, unit) Declarations.pconstant_bodySource
val infer_definition :
sec_univs:UVars.Instance.t option ->
Environ.env ->
Entries.definition_entry ->
HConstr.t option * ('a, unit) Declarations.pconstant_bodySource
val infer_opaque :
sec_univs:UVars.Instance.t option ->
Environ.env ->
'a Entries.opaque_entry ->
(unit, unit) Declarations.pconstant_body * typing_contextSource
val check_delayed :
'a effect_handler ->
typing_context ->
'a Entries.proof_output ->
HConstr.t option * Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes