package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 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.

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.

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

val fix_undefined_variables : t -> t

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.

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

val normalize : t -> t

Return an optimized representation of the input

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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct