package rocq-runtime

  1. Overview
  2. Docs
On This Page
  1. UnivConstraints.
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (6)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.3.0.tar.gz
sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

doc/rocq-runtime.kernel/Univ/index.html

Module UnivSource

Sourcemodule UGlobal : sig ... end

Qualified global universe level

Sourcemodule Level : sig ... end

Universes.

Sourcemodule Universe : sig ... end

univ_level_mem l u Is l is mentioned in u ?

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

univ_level_rem u v min removes u from v, resulting in min if v was exactly u.

Sourceval univ_level_rem : Level.t -> Universe.t -> Universe.t -> Universe.t
UnivConstraints.
Sourcemodule UnivConstraint : sig ... end
Sourcemodule UnivConstraints : sig ... end
Sourcetype 'a constraint_function = 'a -> 'a -> UnivConstraints.t -> UnivConstraints.t

Enforcing UnivConstraints.t.

Sourceval enforce_eq_level : Level.t constraint_function
Sourceval enforce_leq_level : Level.t constraint_function

Universe contexts (as sets)

A set of universes with universe UnivConstraints.t. We linearize the set to a list after typechecking. Beware, representation could change.

Sourcemodule ContextSet : sig ... end