Module `UGraph`Source

Sourcetype t

Graphs of universes.

Sourceval set_cumulative_sprop : bool -> t -> t

Makes the system incomplete.

Sourceval set_type_in_type : bool -> t -> t

Sourceval 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.

Sourceval cumulative_sprop : t -> bool

Sourcetype 'a check_function = t -> 'a -> 'a -> bool

Sourceval check_leq : Univ.Universe.t check_function

Sourceval check_eq : Univ.Universe.t check_function

Sourceval check_eq_level : Univ.Level.t check_function

Sourceval initial_universes : t

The initial graph of universes: Prop < Set

Sourceval initial_universes_with : t -> t

Initial universes, but keeping options such as type in type from the argument.

Sourceval check_eq_instances : Univ.Instance.t check_function

Check equality of instances w.r.t. a universe graph

...

Merge of constraints in a universes graph. The function merge_constraints merges a set of constraints in a given universes graph. It raises the exception UniverseInconsistency if the constraints are not satisfiable.

Source

type univ_inconsistency =
  Univ.constraint_type * Sorts.t * Sorts.t * Univ.explanation Lazy.t option

Sourceexception UniverseInconsistency of univ_inconsistency

Sourceval enforce_constraint : Univ.univ_constraint -> t -> t

Sourceval merge_constraints : Univ.Constraints.t -> t -> t

Sourceval check_constraint : t -> Univ.univ_constraint -> bool

Sourceval check_constraints : Univ.Constraints.t -> t -> bool

Sourceval check_eq_sort : t -> Sorts.t -> Sorts.t -> bool

Sourceval check_leq_sort : t -> Sorts.t -> Sorts.t -> bool

Source

val enforce_leq_alg : 
  Univ.Universe.t ->
  Univ.Universe.t ->
  t ->
  Univ.Constraints.t * t

Adds a universe to the graph, ensuring it is >= or > Set.

raises AlreadyDeclared
if the level is already declared in the graph.

Sourceexception AlreadyDeclared

Sourcemodule Bound : sig ... end

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

Sourceexception UndeclaredLevel of Univ.Level.t

Check that the universe levels are declared. Otherwise

raises UndeclaredLevel
l for the first undeclared level found.

Sourceval check_declared_universes : t -> Univ.Level.Set.t -> unit

Sourceval empty_universes : t

The empty graph of universes

Sourceval 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.

Sourceval 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.

Sourceval 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.

Sourceval domain : t -> Univ.Level.Set.t

Known universes

Sourceval check_subtype : Univ.AbstractContext.t check_function

check_subtype univ ctx1 ctx2 checks whether ctx2 is an instance of ctx1.

Dumping

Sourcetype node =

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

Sourceval repr : t -> node Univ.Level.Map.t

Pretty-printing of universes.

Sourceval pr_universes : (Univ.Level.t -> Pp.t) -> node Univ.Level.Map.t -> Pp.t

Source

val explain_universe_inconsistency : 
  (Univ.Level.t -> Pp.t) ->
  univ_inconsistency ->
  Pp.t

Sourceval check_universes_invariants : t -> unit

Debugging

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/UGraph/index.html

Module `UGraph`Source

...

Dumping

Pretty-printing of universes.

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/UGraph/index.html

Module UGraphSource

...

Dumping

Pretty-printing of universes.

Module `UGraph`Source