package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'a kernel_conversion_function = Environ.env -> 'a -> 'a -> (unit, unit) Stdlib.result
type 'a extended_conversion_function = ?l2r:bool -> ?reds:TransparentState.t -> Environ.env -> ?evars:CClosure.evar_handler -> 'a -> 'a -> (unit, unit) Stdlib.result
type conv_pb =
  1. | CONV
  2. | CUMUL
type ('a, 'err) universe_compare = {
  1. compare_sorts : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> ('a, 'err option) Stdlib.result;
  2. compare_instances : flex:bool -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) Stdlib.result;
  3. compare_cumul_instances : conv_pb -> UVars.Variance.t array -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) Stdlib.result;
}
type ('a, 'err) universe_state = 'a * ('a, 'err) universe_compare
type ('a, 'err) generic_conversion_function = ('a, 'err) universe_state -> Constr.constr -> Constr.constr -> ('a, 'err option) Stdlib.result
val get_cumulativity_constraints : conv_pb -> UVars.Variance.t array -> UVars.Instance.t -> UVars.Instance.t -> Sorts.QUConstraints.t
val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int
val constructor_cumulativity_arguments : (Declarations.mutual_inductive_body * int * int) -> int
val sort_cmp_universes : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> ('a * ('a, 'err) universe_compare) -> ('a, 'err option) Stdlib.result * ('a, 'err) universe_compare
val convert_instances : flex:bool -> UVars.Instance.t -> UVars.Instance.t -> ('a * ('a, 'err) universe_compare) -> ('a, 'err option) Stdlib.result * ('a, 'err) universe_compare
val checked_universes : (UGraph.t, 'err) universe_compare

This function never returns an non-empty error.

These two functions can only fail with unit

val 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).

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct