package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

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

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.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

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
Constraints.
Sourcetype constraint_type = AcyclicGraph.constraint_type =
  1. | Lt
  2. | Le
  3. | Eq
Sourcetype univ_constraint = Level.t * constraint_type * Level.t
Sourcemodule Constraints : sig ... end
Sourcetype 'a constrained = 'a * Constraints.t

A value with universe Constraints.t.

Sourceval constraints_of : 'a constrained -> Constraints.t

Constrained

Sourcetype 'a constraint_function = 'a -> 'a -> Constraints.t -> Constraints.t

Enforcing Constraints.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 Constraints.t. We linearize the set to a list after typechecking. Beware, representation could change.

Sourcemodule ContextSet : sig ... end
Sourcetype 'a in_universe_context_set = 'a * ContextSet.t

A value in a universe context set.

Substitution
Sourcetype universe_level_subst = Level.t Level.Map.t
Sourceval empty_level_subst : universe_level_subst
Sourceval is_empty_level_subst : universe_level_subst -> bool
Sourceval subst_univs_level_level : universe_level_subst -> Level.t -> Level.t

Substitution of universes.

Sourceval subst_univs_level_universe : universe_level_subst -> Universe.t -> Universe.t
Sourceval subst_univs_level_constraints : universe_level_subst -> Constraints.t -> Constraints.t
Pretty-printing of universes.
Sourceval pr_constraint_type : constraint_type -> Pp.t
Sourceval pr_universe_level_subst : (Level.t -> Pp.t) -> universe_level_subst -> Pp.t