package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2
doc/coq-core.kernel/Conversion/index.html
Module ConversionSource
Source
type 'a extended_conversion_function =
?l2r:bool ->
?reds:TransparentState.t ->
Environ.env ->
?evars:CClosure.evar_handler ->
'a ->
'a ->
(unit, unit) resultSource
type ('a, 'err) universe_compare = {compare_sorts : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> ('a, 'err option) result;compare_instances : flex:bool -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;compare_cumul_instances : conv_pb -> UVars.Variance.t array -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
}Source
type ('a, 'err) generic_conversion_function =
('a, 'err) universe_state ->
Constr.constr ->
Constr.constr ->
('a, 'err option) resultSource
val get_cumulativity_constraints :
conv_pb ->
UVars.Variance.t array ->
UVars.Instance.t ->
UVars.Instance.t ->
Sorts.QUConstraints.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, 'err) universe_compare) ->
('a, 'err option) result * ('a, 'err) universe_compareSource
val convert_instances :
flex:bool ->
UVars.Instance.t ->
UVars.Instance.t ->
('a * ('a, 'err) universe_compare) ->
('a, 'err option) result * ('a, 'err) universe_compareThis function never returns an non-empty error.
These two functions can only fail with unit
Source
val generic_conv :
conv_pb ->
l2r:bool ->
TransparentState.t ->
Environ.env ->
?evars:CClosure.evar_handler ->
('a, 'err) generic_conversion_functionThe failure values depend on the universe state functions (for better error messages).