`UnivFlex`

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.

`val empty : t`

`val is_empty : t -> bool`

`val domain : t -> Univ.Level.Set.t`

Contains both defined and undefined flexible levels.

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

For universe minimization.

`val mem : Univ.Level.t -> t -> bool`

Returns `true`

for both defined and undefined flexible levels.

`val is_algebraic : Univ.Level.t -> t -> bool`

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

`val make_nonalgebraic_variable : t -> Univ.Level.t -> t`

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

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

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

`val add : Univ.Level.t -> algebraic:bool -> t -> t`

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

`val add_levels : Univ.Level.Set.t -> algebraic:bool -> t -> t`

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

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

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

.

`biased_union x y`

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

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

`val normalize_univ_variable : t -> UnivSubst.universe_subst_fn`

Apply the substitution to a variable.

`val normalize_universe : t -> Univ.Universe.t -> Univ.Universe.t`

Apply the substitution to an algebraic universe.

`val pr : (Univ.Level.t -> Pp.t) -> t -> Pp.t`

"Show Universes"-style printing.