package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
doc/coq-core.kernel/Term_typing/index.html
Module Term_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 translate_local_def :
Environ.env ->
Names.Id.t ->
Entries.section_def_entry ->
Constr.constr * Sorts.relevance * Constr.typesSource
val translate_constant :
sec_univs:Univ.Level.t array option ->
Environ.env ->
Names.Constant.t ->
Entries.constant_entry ->
'a Declarations.pconstant_bodySource
val translate_opaque :
sec_univs:Univ.Level.t array option ->
Environ.env ->
Names.Constant.t ->
'a Entries.opaque_entry ->
unit Declarations.pconstant_body * typing_contextSource
val check_delayed :
'a effect_handler ->
typing_context ->
'a Entries.proof_output ->
Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universesInternal functions, mentioned here for debug purpose only
Source
val infer_constant :
sec_univs:Univ.Level.t array option ->
Environ.env ->
Entries.constant_entry ->
typing_context Discharge.resultSource
val build_constant_declaration :
Environ.env ->
'a Discharge.result ->
'a Declarations.pconstant_body