package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'a effect_handler = Environ.env -> Constr.t -> 'a -> Constr.t * Univ.ContextSet.t * int

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.

type typing_context
val translate_local_assum : Environ.env -> Constr.types -> Constr.types * Sorts.relevance
val translate_constant : sec_univs:Univ.Level.t array option -> Environ.env -> Names.Constant.t -> Entries.constant_entry -> 'a Declarations.pconstant_body
val translate_opaque : sec_univs:Univ.Level.t array option -> Environ.env -> Names.Constant.t -> 'a Entries.opaque_entry -> unit Declarations.pconstant_body * typing_context

Internal functions, mentioned here for debug purpose only

val infer_constant : sec_univs:Univ.Level.t array option -> Environ.env -> Entries.constant_entry -> typing_context Discharge.result
val build_constant_declaration : Environ.env -> 'a Discharge.result -> 'a Declarations.pconstant_body
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct