package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module UGraphSource

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.

Sourcetype 'a check_function = t -> 'a -> 'a -> bool
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.

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

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

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

Sourceexception AlreadyDeclared
Sourcemodule Bound : sig ... end
Sourceval add_universe : Univ.Level.t -> lbound:Bound.t -> strict:bool -> t -> t
Sourceval add_universe_unconstrained : Univ.Level.t -> t -> t

Add a universe without (Prop,Set) <= u

Sourceexception UndeclaredLevel of Univ.Level.t

Check that the universe levels are declared. Otherwise

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

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

Dumping
Sourcetype node =
  1. | Alias of Univ.Level.t
  2. | Node of bool Univ.Level.Map.t
    (*

    Nodes v s.t. u < v (true) or u <= v (false)

    *)
Pretty-printing of universes.
Sourceval pr_universes : (Univ.Level.t -> Pp.t) -> node Univ.Level.Map.t -> Pp.t
Sourceval check_universes_invariants : t -> unit

Debugging

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