package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
rocq-9.1.1.tar.gz
sha256=35cd03fc4193969b1cce01190340e5c129c1ba8f02242a9e6dff4b83be118759
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