Module `UGraph`

val set_type_in_type : bool -> t -> t

val type_in_type : t -> bool

When type_in_type, functions adding constraints do not fail and may instead ignore inconsistent constraints.

Checking functions such as check_leq always return true.

val initial_universes_with : t -> t: Initial universes, but keeping options such as type in type from the argument.

val check_eq_instances : UVars.Instance.t check_function: Check equality of instances w.r.t. a universe graph

type path_explanation
type explanation = | Path of path_explanation | Other of Pp.t
type univ_inconsistency = Univ.constraint_type * Sorts.t * Sorts.t * explanation option

val enforce_constraint : Univ.univ_constraint -> t -> t
val merge_constraints : Univ.Constraints.t -> t -> t
val check_constraint : t -> Univ.univ_constraint -> bool
val check_constraints : Univ.Constraints.t -> t -> bool
val check_eq_sort : t -> Sorts.t -> Sorts.t -> bool
val check_leq_sort : t -> Sorts.t -> Sorts.t -> bool
val enforce_leq_alg : Univ.Universe.t -> Univ.Universe.t -> t -> Univ.Constraints.t * t

module Bound : sig ... end

val add_universe : Univ.Level.t -> lbound:Bound.t -> strict:bool -> t -> t

exception UndeclaredLevel of Univ.Level.t

Check that the universe levels are declared. Otherwise

val constraints_of_universes : t -> Univ.Constraints.t * Univ.Level.Set.t list: constraints_of_universes g returns csts and partition where csts are the non-Eq constraints and partition is the partition of the universes into equivalence classes.

val choose : (Univ.Level.t -> bool) -> t -> Univ.Level.t -> Univ.Level.t option: choose p g u picks a universe verifying p and equal to u in g.

val constraints_for : kept:Univ.Level.Set.t -> t -> Univ.Constraints.t

constraints_for ~kept g returns the constraints about the universes kept in g up to transitivity.

eg if g is a <= b <= c then constraints_for ~kept:{a, c} g is a <= c.

val check_subtype : UVars.AbstractContext.t check_function: check_subtype univ ctx1 ctx2 checks whether ctx2 is an instance of ctx1.

type node = | Alias of Univ.Level.t | Node of bool Univ.Level.Map.t Nodes v s.t. u < v (true) or u <= v (false)

val pr_universes : (Univ.Level.t -> Pp.t) -> node Univ.Level.Map.t -> Pp.t
val explain_universe_inconsistency : (Sorts.QVar.t -> Pp.t) -> (Univ.Level.t -> Pp.t) -> univ_inconsistency -> Pp.t
val check_universes_invariants : t -> unit: Debugging

`\|` `Alias of Univ.Level.t`
`\|` `Node of bool Univ.Level.Map.t`	Nodes v s.t. u < v (true) or u <= v (false)