package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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 CClosure.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 -> UVars.Instance.t -> UVars.Instance.t -> 'a -> 'a;
  3. compare_cumul_instances : conv_pb -> UVars.Variance.t array -> UVars.Instance.t -> UVars.Instance.t -> 'a -> 'a;
}
Sourcetype 'a universe_state = 'a * 'a universe_compare
Sourcetype 'b generic_conversion_function = 'b universe_state -> Constr.constr -> Constr.constr -> 'b
Sourcetype 'a infer_conversion_function = Environ.env -> 'a -> 'a -> Univ.Constraints.t
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 universe_compare) -> 'a * 'a universe_compare
Sourceval convert_instances : flex:bool -> UVars.Instance.t -> UVars.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).

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