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.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50

doc/coq-core.kernel/Conversion/index.html

Module ConversionSource

Sourceexception NotConvertible
Sourcetype 'a kernel_conversion_function = Environ.env -> 'a -> 'a -> unit
Sourcetype 'a extended_conversion_function = ?l2r:bool -> ?reds:TransparentState.t -> Environ.env -> ?evars:Constr.constr Constr.evar_handler -> 'a -> 'a -> unit
Sourcetype conv_pb =
  1. | CONV
  2. | CUMUL
Sourcetype 'a universe_compare = {
  1. compare_sorts : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
  2. compare_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
  3. compare_cumul_instances : conv_pb -> Univ.Variance.t array -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
}
Sourcetype 'a universe_state = 'a * 'a universe_compare
Sourcetype ('a, 'b) generic_conversion_function = Environ.env -> 'b universe_state -> 'a -> 'a -> 'b
Sourcetype 'a infer_conversion_function = Environ.env -> 'a -> 'a -> Univ.Constraints.t
Sourceval get_cumulativity_constraints : conv_pb -> Univ.Variance.t array -> Univ.Instance.t -> Univ.Instance.t -> Univ.Constraints.t
Sourceval inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int
Sourceval constructor_cumulativity_arguments : (Declarations.mutual_inductive_body * int * int) -> int
Sourceval sort_cmp_universes : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> ('a * 'a universe_compare) -> 'a * 'a universe_compare
Sourceval convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> ('a * 'a universe_compare) -> 'a * 'a universe_compare
Sourceval checked_universes : UGraph.t universe_compare

This function never raise UnivInconsistency.

These two functions can only raise NotConvertible

Depending on the universe state functions, this might raise UniverseInconsistency in addition to NotConvertible (for better error messages).