package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
doc/coq-core.kernel/Conversion/index.html
Module ConversionSource
Source
type 'a extended_conversion_function =
?l2r:bool ->
?reds:TransparentState.t ->
Environ.env ->
?evars:Constr.constr Constr.evar_handler ->
'a ->
'a ->
unitSource
type 'a universe_compare = {compare_sorts : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;compare_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;compare_cumul_instances : conv_pb -> Univ.Variance.t array -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
}Source
type ('a, 'b) generic_conversion_function =
Environ.env ->
'b universe_state ->
'a ->
'a ->
'bSource
val get_cumulativity_constraints :
conv_pb ->
Univ.Variance.t array ->
Univ.Instance.t ->
Univ.Instance.t ->
Univ.Constraints.tSource
val constructor_cumulativity_arguments :
(Declarations.mutual_inductive_body * int * int) ->
intSource
val sort_cmp_universes :
Environ.env ->
conv_pb ->
Sorts.t ->
Sorts.t ->
('a * 'a universe_compare) ->
'a * 'a universe_compareSource
val convert_instances :
flex:bool ->
Univ.Instance.t ->
Univ.Instance.t ->
('a * 'a universe_compare) ->
'a * 'a universe_compareThis function never raise UnivInconsistency.
These two functions can only raise NotConvertible
Source
val generic_conv :
conv_pb ->
l2r:bool ->
Constr.constr Constr.evar_handler ->
TransparentState.t ->
(Constr.constr, 'a) generic_conversion_functionDepending on the universe state functions, this might raise UniverseInconsistency in addition to NotConvertible (for better error messages).