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

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
type universe_opt_subst = Univ.Universe.t option universe_map
val normalize_univ_variable_opt_subst : universe_opt_subst -> Univ.Level.t -> Univ.Universe.t option
val normalize_universe_opt_subst : universe_opt_subst -> Univ.Universe.t -> Univ.Universe.t
val normalize_opt_subst : universe_opt_subst -> universe_opt_subst

Full universes substitutions into terms

val nf_evars_and_universes_opt_subst : (Constr.existential -> Constr.constr option) -> (Univ.Level.t -> Univ.Level.t) -> (Sorts.t -> Sorts.t) -> (Sorts.relevance -> Sorts.relevance) -> Constr.constr -> Constr.constr
val subst_univs_universe : (Univ.Level.t -> Univ.Universe.t option) -> 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