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 (5)

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.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

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

Module UVarsSource

Support for universe polymorphism
Sourcemodule Variance : sig ... end
Universe instances
Sourcemodule Instance : sig ... end
Sourceval eq_sizes : (int * int) -> (int * int) -> bool

Convenient function to compare the result of Instance.length, UContext.size etc

Sourcetype 'a pconstraints_function = 'a -> 'a -> (QPairSet.t * Univ.UnivConstraints.t) -> QPairSet.t * Univ.UnivConstraints.t
Sourceval enforce_eq_instances : Instance.t pconstraints_function
Sourceval enforce_eq_variance_instances : Variance.t array -> Instance.t pconstraints_function
Sourceval enforce_leq_variance_instances : Variance.t array -> Instance.t pconstraints_function
Sourcetype 'a puniverses = 'a * Instance.t
Sourceval out_punivs : 'a puniverses -> 'a
Sourceval in_punivs : 'a -> 'a puniverses
Sourceval eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool
Sourcetype bound_names = {
  1. quals : Names.Name.t array;
  2. univs : Names.Name.t array;
}
Sourceval empty_bound_names : bound_names

A vector of universe levels with universe PConstraints.t, representing local universe variables and associated PConstraints.t; the names are user-facing names for printing

Sourcemodule UContext : sig ... end

A value in a universe context.

Sourcetype 'a in_universe_context = 'a * UContext.t

A value in a universe context.

Sourcemodule AbstractContext : sig ... end
Sourcetype 'a univ_abstracted = {
  1. univ_abstracted_value : 'a;
  2. univ_abstracted_binder : AbstractContext.t;
}

A value with bound universe levels.

Sourceval map_univ_abstracted : ('a -> 'b) -> 'a univ_abstracted -> 'b univ_abstracted
Substitution
Sourcetype universe_level_subst = Univ.Level.t Univ.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 -> Univ.Level.t -> Univ.Level.t

Substitution of universes.

Sourceval subst_univs_level_universe : universe_level_subst -> Univ.Universe.t -> Univ.Universe.t
Sourceval subst_poly_constraints : sort_level_subst -> PConstraints.t -> PConstraints.t
Sourceval pr_universe_level_subst : (Univ.Level.t -> Pp.t) -> universe_level_subst -> Pp.t
Sourceval pr_quality_level_subst : (Sorts.QVar.t -> Pp.t) -> Sorts.Quality.t Sorts.QVar.Map.t -> Pp.t
Sourceval empty_sort_subst : sort_level_subst
Sourceval is_empty_sort_subst : sort_level_subst -> bool
Sourceval subst_univs_level_abstract_universe_context : sort_level_subst -> AbstractContext.t -> AbstractContext.t

There are no constraints on qualities, so this only needs a subst for univs

Sourceval subst_sort_level_instance : sort_level_subst -> Instance.t -> Instance.t

Level to universe substitutions.

Sourceval subst_sort_level_quality : sort_level_subst -> Sorts.Quality.t -> Sorts.Quality.t
Sourceval subst_sort_level_sort : sort_level_subst -> Sorts.t -> Sorts.t
Sourceval subst_sort_level_relevance : sort_level_subst -> Sorts.relevance -> Sorts.relevance
Sourceval subst_instance_instance : Instance.t -> Instance.t -> Instance.t

Substitution of instances

Sourceval subst_instance_universe : Instance.t -> Univ.Universe.t -> Univ.Universe.t
Sourceval subst_instance_quality : Instance.t -> Sorts.Quality.t -> Sorts.Quality.t
Sourceval subst_instance_sort : Instance.t -> Sorts.t -> Sorts.t
Sourceval subst_instance_relevance : Instance.t -> Sorts.relevance -> Sorts.relevance
Sourceval subst_instance_sort_level_subst : Instance.t -> sort_level_subst -> sort_level_subst
Sourceval make_instance_subst : Instance.t -> sort_level_subst

Creates u(0) ↦ 0; ...; u(n-1) ↦ n - 1 out of u(0); ...; u(n - 1)

Sourceval abstract_universes : UContext.t -> Instance.t * AbstractContext.t

TODO: move universe abstraction out of the kernel

Sourceval make_abstract_instance : AbstractContext.t -> Instance.t