package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b

doc/coq-core.pretyping/Coercionops/index.html

Module CoercionopsSource

Sourcetype 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

Sourceval cl_typ_eq : cl_typ -> cl_typ -> bool

Equality over cl_typ

Sourceval cl_typ_ord : cl_typ -> cl_typ -> int

Comparison of cl_typ

Sourcetype coe_typ = Names.GlobRef.t

This is the type of coercion kinds

Sourcetype 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

Sourcetype inheritance_path = coe_info_typ list

This is the type of paths from a class to another

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

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

raises Not_found if not convertible to a class

Sourceval declare_coercion : Environ.env -> Evd.evar_map -> ?update:bool -> coe_info_typ -> unit

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

Sourceval coercion_exists : coe_typ -> bool

Access to coercions infos

Sourceval 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

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

This is for printing purpose

Sourceval pr_class : cl_typ -> Pp.t
Sourceval inheritance_graph : unit -> ((cl_typ * cl_typ) * inheritance_path) list
Sourceval classes : unit -> cl_typ list
Sourceval coercions : unit -> coe_info_typ list
Sourceval 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
Sourceval reachable_from : cl_typ -> ClTypSet.t