package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type cl_typ =
  1. | CL_SORT
  2. | CL_FUN
  3. | CL_SECVAR of Names.variable
  4. | CL_CONST of Names.Constant.t
  5. | CL_IND of Names.inductive
  6. | CL_PROJ of Names.Projection.Repr.t
val cl_typ_eq : cl_typ -> cl_typ -> bool
val subst_cl_typ : Mod_subst.substitution -> cl_typ -> cl_typ
val cl_typ_ord : cl_typ -> cl_typ -> int
type cl_info_typ = {
  1. cl_param : int;
}
type coe_typ = Names.GlobRef.t
type coe_info_typ = {
  1. coe_value : Names.GlobRef.t;
  2. coe_local : bool;
  3. coe_is_identity : bool;
  4. coe_is_projection : Names.Projection.Repr.t option;
  5. coe_param : int;
}
type cl_index
type inheritance_path = coe_info_typ list
val class_exists : cl_typ -> bool
val class_info : cl_typ -> cl_index * cl_info_typ
val class_info_from_index : cl_index -> cl_typ * cl_info_typ
val inductive_class_of : Names.inductive -> cl_index
val class_args_of : Environ.env -> Evd.evar_map -> EConstr.types -> EConstr.constr list
type coercion = {
  1. coercion_type : coe_typ;
  2. coercion_local : bool;
  3. coercion_is_id : bool;
  4. coercion_is_proj : Names.Projection.Repr.t option;
  5. coercion_source : cl_typ;
  6. coercion_target : cl_typ;
  7. coercion_params : int;
}
val subst_coercion : Mod_subst.substitution -> coercion -> coercion
val declare_coercion : Environ.env -> Evd.evar_map -> coercion -> unit
val coercion_exists : coe_typ -> bool
val lookup_path_between_class : (cl_index * cl_index) -> inheritance_path
val lookup_path_to_fun_from : Environ.env -> Evd.evar_map -> EConstr.types -> EConstr.types * inheritance_path
val lookup_path_to_sort_from : Environ.env -> Evd.evar_map -> EConstr.types -> EConstr.types * inheritance_path
val lookup_pattern_path_between : Environ.env -> (Names.inductive * Names.inductive) -> (Names.constructor * int) list
val install_path_printer : (((cl_index * cl_index) * inheritance_path) -> Pp.t) -> unit
val install_path_comparator : (Environ.env -> Evd.evar_map -> inheritance_path -> inheritance_path -> bool) -> unit
val string_of_class : cl_typ -> string
val pr_class : cl_typ -> Pp.t
val pr_cl_index : cl_index -> Pp.t
val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
val classes : unit -> cl_typ list
val coercions : unit -> coe_info_typ list
val hide_coercion : coe_typ -> int option
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