package coq

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

Graphs of universes.

val set_cumulative_sprop : bool -> t -> t

Makes the system incomplete.

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.

type 'a check_function = t -> 'a -> 'a -> bool
val check_eq_level : Univ.Level.t check_function
val initial_universes : t

The initial graph of universes: Prop < Set

val initial_universes_with : t -> t

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

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

val enforce_constraint : Univ.univ_constraint -> t -> t
val merge_constraints : Univ.Constraint.t -> t -> t
val check_constraint : t -> Univ.univ_constraint -> bool
val check_constraints : Univ.Constraint.t -> t -> bool
val enforce_leq_alg : Univ.Universe.t -> Univ.Universe.t -> t -> Univ.Constraint.t * t

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

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

exception AlreadyDeclared
module Bound : sig ... end
val add_universe : Univ.Level.t -> lbound:Bound.t -> strict:bool -> t -> t
val add_universe_unconstrained : Univ.Level.t -> t -> t

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

exception UndeclaredLevel of Univ.Level.t

Check that the universe levels are declared. Otherwise

val check_declared_universes : t -> Univ.LSet.t -> unit
val empty_universes : t

The empty graph of universes

val constraints_of_universes : t -> Univ.Constraint.t * Univ.LSet.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.LSet.t -> t -> Univ.Constraint.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 domain : t -> Univ.LSet.t

Known universes

val check_subtype : lbound:Bound.t -> Univ.AUContext.t check_function

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

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

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

    *)
val repr : t -> node Univ.LMap.t
Pretty-printing of universes.
val pr_universes : (Univ.Level.t -> Pp.t) -> node Univ.LMap.t -> Pp.t
val 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