package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.kernel/Conversion/index.html

Module ConversionSource

Sourcetype 'a kernel_conversion_function = Environ.env -> 'a -> 'a -> (unit, unit) result
Sourcetype 'a extended_conversion_function = ?l2r:bool -> ?reds:TransparentState.t -> Environ.env -> ?evars:CClosure.evar_handler -> 'a -> 'a -> (unit, unit) result
Sourcetype conv_pb =
  1. | CONV
  2. | CUMUL
Sourcetype ('a, 'err) universe_compare = {
  1. compare_sorts : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> ('a, 'err option) result;
  2. compare_instances : flex:bool -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
  3. compare_cumul_instances : conv_pb -> UVars.Variance.t array -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
}
Sourcetype ('a, 'err) universe_state = 'a * ('a, 'err) universe_compare
Sourcetype ('a, 'err) generic_conversion_function = ('a, 'err) universe_state -> Constr.constr -> Constr.constr -> ('a, 'err option) result
Sourceval get_cumulativity_constraints : conv_pb -> UVars.Variance.t array -> UVars.Instance.t -> UVars.Instance.t -> Sorts.QUConstraints.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, 'err) universe_compare) -> ('a, 'err option) result * ('a, 'err) universe_compare
Sourceval convert_instances : flex:bool -> UVars.Instance.t -> UVars.Instance.t -> ('a * ('a, 'err) universe_compare) -> ('a, 'err option) result * ('a, 'err) universe_compare
Sourceval checked_universes : (UGraph.t, 'err) universe_compare

This function never returns an non-empty error.

These two functions can only fail with unit

Sourceval generic_conv : conv_pb -> l2r:bool -> TransparentState.t -> Environ.env -> ?evars:CClosure.evar_handler -> ('a, 'err) generic_conversion_function

The failure values depend on the universe state functions (for better error messages).