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.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.engine/UnivFlex/index.html

Module UnivFlexSource

Sourcetype t

Flexible universe data. A level is flexible if UnivFlex.mem returns true on it. Flexible levels may have a definition, this induces a universe substitution.

Only some flexible levels may be defined as algebraic universes.

Sourceval empty : t
Sourceval is_empty : t -> bool
Sourceval domain : t -> Univ.Level.Set.t

Contains both defined and undefined flexible levels.

Sourceval fold : (Univ.Level.t -> is_defined:bool -> 'a -> 'a) -> t -> 'a -> 'a

For universe minimization.

Sourceval mem : Univ.Level.t -> t -> bool

Returns true for both defined and undefined flexible levels.

Sourceval is_algebraic : Univ.Level.t -> t -> bool

Is the level allowed to be defined by an algebraic universe?

Sourceval make_nonalgebraic_variable : t -> Univ.Level.t -> t

Make the level non algebraic. Undefined behaviour on already-defined algebraics.

Sourceval make_all_undefined_nonalgebraic : t -> t

Turn all undefined flexible algebraic variables into simply flexible ones. Can be used in case the variables might appear in universe instances (typically for polymorphic program obligations).

Sourceval fix_undefined_variables : t -> t

Make all undefined flexible levels into rigid levels, ie remove them.

Sourceval add : Univ.Level.t -> algebraic:bool -> t -> t

Makes a level flexible with no definition. It must not already be flexible.

Sourceval remove : Univ.Level.t -> t -> t
Sourceval add_levels : Univ.Level.Set.t -> algebraic:bool -> t -> t

Make the levels flexible with no definitions. They must not already be flexible.

Sourceval define : Univ.Level.t -> Univ.Universe.t -> t -> t

Define the level to the given universe. The level must already be flexible and must be undefined.

Sourceval constrain_variables : Univ.Level.Set.t -> t -> Univ.ContextSet.t -> Univ.ContextSet.t * t

constrain_variables diff subst ctx removes bindings l := l' from the substitution where l is in diff and l' is a level, and adds l, l = l' to ctx.

Sourceval biased_union : t -> t -> t

biased_union x y favors the bindings of the first map that are defined, otherwise takes the second's bindings.

Sourceval normalize : t -> t

Return an optimized representation of the input

Sourceval normalize_univ_variables : t -> t * Univ.Level.Set.t * UnivSubst.universe_subst_fn

As normalize and also returns the set of defined variables and a function which is equivalent to calling normalize_univ_variable on the substitution but may be faster.

Sourceval normalize_univ_variable : t -> UnivSubst.universe_subst_fn

Apply the substitution to a variable.

Sourceval normalize_universe : t -> Univ.Universe.t -> Univ.Universe.t

Apply the substitution to an algebraic universe.

Sourceval pr : (Univ.Level.t -> Pp.t) -> t -> Pp.t

"Show Universes"-style printing.