Module `Univ`

module UGlobal : sig ... end: Qualified global universe level

module Level : sig ... end: Universes.

module Universe : sig ... end

val univ_level_mem : Level.t -> Universe.t -> bool

val univ_level_rem : Level.t -> Universe.t -> Universe.t -> Universe.t

Constraints.

type constraint_type = AcyclicGraph.constraint_type = | Lt | Le | Eq
type univ_constraint = Level.t * constraint_type * Level.t

module Constraints : sig ... end

type 'a constrained = 'a * Constraints.t: A value with universe Constraints.t.

val constraints_of : 'a constrained -> Constraints.t: Constrained

type 'a constraint_function = 'a -> 'a -> Constraints.t -> Constraints.t: Enforcing Constraints.t.

val enforce_eq_level : Level.t constraint_function
val enforce_leq_level : Level.t constraint_function

module ContextSet : sig ... end

type 'a in_universe_context_set = 'a * ContextSet.t: A value in a universe context set.

Substitution

type universe_level_subst = Level.t Level.Map.t

val empty_level_subst : universe_level_subst
val is_empty_level_subst : universe_level_subst -> bool
val subst_univs_level_level : universe_level_subst -> Level.t -> Level.t: Substitution of universes.

val subst_univs_level_universe : universe_level_subst -> Universe.t -> Universe.t
val subst_univs_level_constraints : universe_level_subst -> Constraints.t -> Constraints.t

Pretty-printing of universes.

val pr_constraint_type : constraint_type -> Pp.t
val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t
val pr_universe_level_subst : (Level.t -> Pp.t) -> universe_level_subst -> Pp.t

Hash-consing

val hcons_univ : Universe.t -> Universe.t
val hcons_constraints : Constraints.t -> Constraints.t
val hcons_universe_set : Level.Set.t -> Level.Set.t
val hcons_universe_context_set : ContextSet.t -> ContextSet.t