package coq-core

  1. Overview
  2. Docs
package coq-core
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

This is the type of class kinds

val cl_typ_eq : cl_typ -> cl_typ -> bool

Equality over cl_typ

val subst_cl_typ : Environ.env -> Mod_subst.substitution -> cl_typ -> cl_typ
val cl_typ_ord : cl_typ -> cl_typ -> int

Comparison of cl_typ

type coe_typ = Names.GlobRef.t

This is the type of coercion kinds

type coe_info_typ = {
  1. coe_value : Names.GlobRef.t;
  2. coe_typ : Constr.t;
  3. coe_local : bool;
  4. coe_reversible : bool;
  5. coe_is_identity : bool;
  6. coe_is_projection : Names.Projection.Repr.t option;
  7. coe_source : cl_typ;
  8. coe_target : cl_typ;
  9. coe_param : int;
}

This is the type of infos for declared coercions

type inheritance_path = coe_info_typ list

This is the type of paths from a class to another

Access to classes infos
val class_exists : cl_typ -> bool
val class_nparams : cl_typ -> int

find_class_type env sigma c returns the head reference of c, its universe instance and its arguments

val find_class_glob_type : 'a Glob_term.glob_constr_g -> cl_typ

raises Not_found if not convertible to a class

val class_args_of : Environ.env -> Evd.evar_map -> EConstr.types -> EConstr.constr list
val declare_coercion : Environ.env -> Evd.evar_map -> ?update:bool -> coe_info_typ -> unit

Set update to update an already declared coercion (default false).

val coercion_exists : coe_typ -> bool

Access to coercions infos

val coercion_info : coe_typ -> coe_info_typ
Lookup functions for coercion paths
  • raises Not_found

    in the following functions when no path exists

given one (or two) types these function also return the class (classes) of the type and its class_args_of

val lookup_path_between_class : (cl_typ * cl_typ) -> inheritance_path
val lookup_path_between : Environ.env -> Evd.evar_map -> src:EConstr.types -> tgt:EConstr.types -> inheritance_path
val lookup_path_to_fun_from : Environ.env -> Evd.evar_map -> EConstr.types -> inheritance_path
val lookup_path_to_sort_from : Environ.env -> Evd.evar_map -> EConstr.types -> inheritance_path
val lookup_pattern_path_between : Environ.env -> (Names.inductive * Names.inductive) -> (Names.constructor * int) list
val path_is_reversible : inheritance_path -> bool
val string_of_class : cl_typ -> string

This is for printing purpose

val pr_class : cl_typ -> Pp.t
val inheritance_graph : unit -> ((cl_typ * cl_typ) * inheritance_path) list
val classes : unit -> cl_typ list
val coercions : unit -> coe_info_typ list
val hide_coercion : coe_typ -> int option

hide_coercion returns the number of params to skip if the coercion must be hidden, None otherwise; it raises Not_found if not a coercion

module ClTypSet : Set.S with type elt = cl_typ
val reachable_from : cl_typ -> ClTypSet.t
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