package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

Classes and coercions.

val try_add_new_coercion_with_target : Names.GlobRef.t -> local:bool -> poly:bool -> source:Coercionops.cl_typ -> target:Coercionops.cl_typ -> unit

try_add_new_coercion_with_target ref s src tg declares ref as a coercion from src to tg

val try_add_new_coercion : Names.GlobRef.t -> local:bool -> poly:bool -> unit

try_add_new_coercion ref s declares ref, assumed to be of type (x1:T1)...(xn:Tn)src->tg, as a coercion from src to tg

val try_add_new_coercion_subclass : Coercionops.cl_typ -> local:bool -> poly:bool -> unit

try_add_new_coercion_subclass cst s expects that cst denotes a transparent constant which unfolds to some class tg; it declares an identity coercion from cst to tg, named something like "Id_cst_tg"

val try_add_new_coercion_with_source : Names.GlobRef.t -> local:bool -> poly:bool -> source:Coercionops.cl_typ -> unit

try_add_new_coercion_with_source ref s src declares ref as a coercion from src to tg where the target is inferred from the type of ref

val try_add_new_identity_coercion : Names.Id.t -> local:bool -> poly:bool -> source:Coercionops.cl_typ -> target:Coercionops.cl_typ -> unit

try_add_new_identity_coercion id s src tg enriches the environment with a new definition of name id declared as an identity coercion from src to tg

val add_coercion_hook : poly:bool -> Declare.Hook.t
val add_subclass_hook : poly:bool -> Declare.Hook.t
val class_of_global : Names.GlobRef.t -> Coercionops.cl_typ
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