package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'a universe_map = 'a Univ.Level.Map.t
type universe_subst = Univ.Universe.t universe_map
type universe_subst_fn = Univ.Level.t -> Univ.Universe.t option
type universe_level_subst_fn = Univ.Level.t -> Univ.Level.t
type quality_subst = Sorts.Quality.t Sorts.QVar.Map.t
type quality_subst_fn = Sorts.QVar.t -> Sorts.Quality.t

The resulting function must never be called on a level which would produce an algebraic.

val subst_univs_constraints : universe_subst_fn -> Univ.Constraints.t -> Univ.Constraints.t

Full universes substitutions into terms

val map_universes_opt_subst_with_binders : ('a -> 'a) -> ('a -> Constr.constr -> Constr.constr) -> quality_subst_fn -> universe_subst_fn -> 'a -> Constr.constr -> Constr.constr
val nf_evars_and_universes_opt_subst : (Constr.existential -> Constr.constr option) -> quality_subst_fn -> universe_subst_fn -> Constr.constr -> Constr.constr
  • deprecated Use [UnivSubst.map_universes_opt_subst_with_binders]
val subst_univs_universe : universe_subst_fn -> Univ.Universe.t -> Univ.Universe.t
val pr_universe_subst : (Univ.Level.t -> Pp.t) -> universe_subst -> Pp.t
val enforce_eq_sort : Sorts.t -> Sorts.t -> Univ.Constraints.t -> Univ.Constraints.t
val enforce_leq_sort : Sorts.t -> Sorts.t -> Univ.Constraints.t -> Univ.Constraints.t
val enforce_leq_alg_sort : Sorts.t -> Sorts.t -> UGraph.t -> Univ.Constraints.t * UGraph.t

Picks an arbitrary set of constraints sufficient to ensure u <= v.

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